Don’t perform simplifications with logic of here-and-there #27

New Issue

patrick · 2019-01-16T01:50:08+01:00

patrick commented

2019-01-16 01:50:08 +01:00

Formulas obtained by translation that are subject to the logic of here-and-there and not classical logic aren’t safe to be simplified with the set of all simplification rules that I implemented for the completion-based translation mode. For those, no simplifications should be performed as a first step (and later safe simplifications should be allowed).

patrick added this to the anthem 0.2.0 milestone 2019-01-16 01:50:08 +01:00

patrick self-assigned this 2019-01-16 01:50:08 +01:00

patrick added the

bug

label 2019-01-16 01:50:08 +01:00

patrick changed title from ~~Only perform safe simplifications with logic of here-and-there~~ to Don’t perform simplifications with logic of here-and-there

2019-01-16 02:38:30 +01:00

patrick commented

2019-01-16 02:39:05 +01:00

I implemented this in conjunction with #22.

patrick closed this issue

2019-01-16 02:39:05 +01:00

Sign in to join this conversation.