synasp.pl -- Synthesizing Answer Set Programs

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

Prog

Logic program. List of rules, e.g.

[(p(X) ; not q(X) <-- r(X), not s(X)), (p(X) <-- true), (false <-- q(X)]

Form

First-order formula in Prolog-readable PIE notation.

Options

List of options. Only options processed directly by the predicates in this module are described. The list is passed to underlying layers that do the proving and interpolation.

author

- Christoph Wernhard

 p_gamma(+Prog, -Form) is det

Form is the gamma transformation of Prog.

 p_seq(+Prog1, +Prog2, +Options) is semidet

Succeeds if it can be verified that Prog1 and Prog2 are strongly equivalent.

 f_encodes_p_form(+Form1, -Form2) is det

Form2 is valid iff Form1 encodes a logic program.

 f_decode_p(+Form, -Prog, +Options) is det

Prog is obtained by decoding Form. Processed options include

decode_cnf=CNF

Specifies the variant of CNF transformation. See code for values of CNF.

decode_partition=PM

Specifies the partitioning method (Step 2 of the algorithm). See code for values of PM.

decode_simp=Simp

Specifies simplifications on the CNF before extraction. See code for values of Simp.

 f_lp_ipol_form(+FormF, +FormG, +Options, -FormH) is det

FormH is the formula underlying the Craig-Lyndon interpolation for the LP-interplation of FormF and FormG.

 latest_ipol_form(?Form) is semidet

Form is the formula of the formula of the latest interpolation task. It is asserted before prover invocation. Useful, e.g., for debugging.

 f_lp_ipol(+FormF, +FormG, -FormH, +Options) is nondet

FormH is an LP-interpolant of FormF and FormG.

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.

 p_def(+ProgP, +ProgQ, +Vocab, -ProgR, +Options) is nondet

ProgR is a definiens of ProgQ within ProgP in the vocabulary Vocab.

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.

Arguments:

Vocab

- A list of predicates or a term v(VP,VP1,VN) where VP, VP1 and VN are lists of predicates, corresponding to the position constraining corollary. If the forget option is set, predicates disallowed in positives heads are VP cup VP1 and the predicates disallowed in negative bodies are VP1.

Options

- See examples_synasp.pl for a compilation of useful options. Directly processed options include forget Interpret Vocab as specifying the predicates that are not allowed. lpip_simp_input=Simp Special formula simplification for interpolation arguments. Recognized values of Simp: 0 No special simplification. 1 Simplify the second interpolation argument such that it involves less distinct variables, typically resulting in less Skolem terms. Very useful with CMProver and Prover9. 2 Like 1 but the simplification is also applied to the first interolation argument. lpdef_dry=FormF-FormG Don't perform interpolation but instead return the input formulas to IP-interpolation. lpip_dry=Form Don't perform interpolation but instead return the input to Craig-Lyndon interpolation as implication.

 p_sentails(+Prog1, +Prog2, +Options) is semidet

Succeeds if it can be verified that Prog1 s-entails Prog2.

The underlying notion of entailment (called here "s-entails") can be specified as P ⊧ Q iff P and P∪Q are strongly equivalent.

 p_interpolant(+ProgP, +ProgQ, -ProgR, +Options) is nondet

ProgR is an s-interpolant of ProgP and ProgQ, i.e., a Craig-Lyndon interpolant of two logic programs with respect to s-entailment (see p_sentails/3).

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.