With the new translation scheme, the generated output has to be generally interpreted under the semantics of the logic of here-and-there. Horn programs are an exception because for those, the classical logic and the logic of here-and-there coincide.
However, for programs with negation or choice rules, the translation obtained with the new scheme must not be understood in terms of classical logic. In this case, a warning should be printed that explicitly states that the output is only valid if understood in the logic of here-and-there.
With the new translation scheme, the generated output has to be generally interpreted under the semantics of the logic of here-and-there. Horn programs are an exception because for those, the classical logic and the logic of here-and-there coincide.
However, for programs with negation or choice rules, the translation obtained with the new scheme *must not be understood in terms of classical logic.* In this case, a warning should be printed that explicitly states that the output is only valid if understood in the logic of here-and-there.
patrick
added this to the anthem 0.2.0 milestone 2019-01-13 16:53:04 +01:00
patrick
self-assigned this 2019-01-13 16:53:04 +01:00
Blocking a user prevents them from interacting with repositories, such as opening or commenting on pull requests or issues. Learn more about blocking a user.
With the new translation scheme, the generated output has to be generally interpreted under the semantics of the logic of here-and-there. Horn programs are an exception because for those, the classical logic and the logic of here-and-there coincide.
However, for programs with negation or choice rules, the translation obtained with the new scheme must not be understood in terms of classical logic. In this case, a warning should be printed that explicitly states that the output is only valid if understood in the logic of here-and-there.
Implemented for cases where anthem finds a choice rule or negative literals in bodies.