Prototypical implementation of the approach described in Jan Heuer and Christoph Wernhard: "Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic", 2024.
Installation Notes. Runs in the PIE environment http://cs.christophwernhard.com/pie/ . Tested with SWI-Prolog 9.2.5 and PIE June 2024. Also Prover9/Mace4 is recommended.
Version: Tue Jun 18 15:06:49 2024
Argument Types
[(p(X) ; not q(X) <-- r(X), not s(X)), (p(X) <-- true), (false <-- q(X)]
Succeeds only if the underlying entailment can be proven. Enumerates alternate solutions in case options specify an interpolation method that enumerates different interpolants for different proofs.
Succeeds only if the underlying entailment can be proven. Enumerates alternate solutions in case options specify an interpolation method that enumerates different interpolants for different proofs.
The underlying notion of entailment (called here "s-entails") can be specified as P ⊧ Q iff P and P∪Q are strongly equivalent.
Succeeds only if the underlying entailment can be proven. Enumerates alternate solutions in case options specify an interpolation method that enumerates different interpolants for different proofs.