Implement new translation scheme for Horn programs #21

New Issue

patrick · 2019-01-13T16:47:16+01:00

patrick commented

2019-01-13 16:47:16 +01:00

Vladimir proposed a new translation scheme that isn’t geared towards human-readable output but towards proving program properties or strong equivalence between programs through a translation to the logic of here-and-there.

As a first step, this new translation scheme should be implemented for Horn programs (without negative literals and choice rules).

Vladimir proposed a new translation scheme that isn’t geared towards human-readable output but towards proving program properties or strong equivalence between programs through a translation to the logic of here-and-there. As a first step, this new translation scheme should be implemented for Horn programs (without negative literals and choice rules).

patrick added this to the anthem 0.2.0 milestone 2019-01-13 16:47:16 +01:00

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

patrick added the

enhancement

label 2019-01-13 16:47:16 +01:00

patrick commented

2019-01-16 02:37:36 +01:00

I implemented the full specification in Vladimir’s draft. To account for non-Horn programs, I added a warning in case the output must not be understood in terms of classical logic (#22).

patrick closed this issue

2019-01-16 02:37:36 +01:00

Sign in to join this conversation.