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.0.4 and PIE February 2024. Also Prover9/Mace4 is recommended.
Version: Tue Feb 13 10:54:39 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.