Translate logic of here-and-there to classical logic #23

New Issue

patrick · 2019-01-13T16:56:22+01:00

patrick commented

2019-01-13 16:56:22 +01:00

For non-Horn programs, the output generated by the new translation scheme is subject to the logic of here-and-there. However, there aren’t many tools (less so theorem provers) available to work with output in this form.

For this reason, it would be useful to implement a translation from the logic of here-and-there to classical logic. It might make sense to add an option like --semantics with values classical vs. here-and-there.

For non-Horn programs, the output generated by the new translation scheme is subject to the logic of here-and-there. However, there aren’t many tools (less so theorem provers) available to work with output in this form. For this reason, it would be useful to implement a translation from the logic of here-and-there to classical logic. It might make sense to add an option like `--semantics` with values `classical` vs. `here-and-there`.

patrick added this to the anthem 0.2.1 milestone 2019-01-13 16:56:22 +01:00

patrick self-assigned this 2019-01-13 16:56:22 +01:00

patrick added the

enhancement

label 2019-01-13 16:56:22 +01:00

Sign in to join this conversation.