%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Copyright (C) 2024 Christoph Wernhard
%%%%
%%%% This program is free software: you can redistribute it and/or modify it
%%%% under the terms of the GNU General Public License as published by the
%%%% Free Software Foundation, either version 3 of the License, or (at your
%%%% option) any later version.
%%%%
%%%% This program is distributed in the hope that it will be useful, but
%%%% WITHOUT ANY WARRANTY; without even the implied warranty of
%%%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
%%%% Public License for more details.
%%%%
%%%% You should have received a copy of the GNU General Public License
%%%% along with this program. If not, see .
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Examples for SYNASP
%%%%
%%%% Examples for synasp.pl, the 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.
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Usage:
%%%%
%%%% Requires SWI-Prolog 9.0.4, Prover9 (prover9, mace4, prooftrans commands)
%%%% and PIE (http://cs.christophwernhard.com/pie/)
%%%%
%%%% Load this file into PIE, i.e., start PIE for example with
%%%% $ swipl --stack_limit=12g -f ${PIE}/folelim/load.pl
%%%% and consult this file.
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- use_module(synasp).
%%%%
%%%% Verbosity, default value is 50. A value < 10 suppresses most info about
%%%% printed prover invocation and progress.
%%%%
:- set_info_verbosity(9).
%%%%
%%%% Run all examples.
%%%%
ex_runall :-
get_info_verbosity(V),
format('Verbosity is ~q~n', [V]),
ex_decode,
ex_def.
/*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Some Useful Options for p_def/5
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
forget
Interpret the Vocabulary as specifying the predicates that are *not*
allowed. If the Vocabulary is specified as 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.
timeout=60
Give the prover 60s timeout.
lpip_simp_input=1
lpip_simp_input=2
1: Effects reduced number of different Skolem terms on the right side of
the interpolation entailment. Very useful for CMProver and also Prover9.
With Prover9 it can effect substantially shorter proofs that make
interpolation feasible.
2: Similar simplification also applied to the left side of the
interpolation entailment.
pr_options=[d(1)]
CMProver - iterative deepening increments by 1 instead of growth by a
factor
ip_mode=hyper
Interpolation with CMProver: hyper conversion of the proof before
interpolant extraction.
enum_ips=3
Interpolation with CMProver: Enumerate up to 3 alternate interpolants for
different proofs.
prover=prover9
Use Prover9 instead of CMProver for interpolation.
Knows bugs with Prover9 for interpolation:
In some cases identification of source assumptions to determine the
interpolation side fails and throws an error.
- This seems to happen if Prover9 uses a first-order formula directly as
clausal assumption, without a clausification step.
- This seems also to happen if Prover9 apparently normalizes the input a
bit before processing it. For example, the original input (all A
(((-q0(A) | p0(A)) & (-q1(A) | p1(A))) & ((-p0(A) | r0(A)) & ((-p1(A) |
r1(A)) & ((-q0(A) | r0(A)) & (-q1(A) | r1(A))))))). appears in the INPUT
reported by Prover9 as (all A ((-q0(A) | p0(A)) & (-q1(A) | p1(A)) &
(-p0(A) | r0(A)) & (-p1(A) | r1(A) ) & (-q0(A) | r0(A)) & (-q1(A) |
r1(A)))).
With option "cleanup=false" temporary files for and from prover9 are
preserved (usually in /tmp).
ip_dotgraph=FileName
Write an image file showing the 2-colored clausal tableau underlying
interpolation (requires graphviz installed). Example call with some
further options to get a tableau of reasonable small size:
?- exdef(14-2, P, Q, V),
p_def(P, Q, V, R, [ip_dotgraph='/tmp/proof.png',
pr_options=[d(1)], lpip_simp_input=1]).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*/
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Generally Good Option Settings for CMProver
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
cm_opts(n1, [cm_cfg=lean1, add_cm_options=[r8(al)]]).
cm_opts(n2, [cm_cfg=lean]).
cm_opts(n3, [cm_cfg=low]).
cm_opts(n4, [cm_cfg=lean, add_pr_options=[depth_timeout(2)]]).
cm_opts(n5, [cm_cfg=std, add_cm_options=[hd]-[hd1],
add_pr_options=[depth_timeout(2)]]).
cm_opts(n6, [cm_cfg=std, add_cm_options=[hd]-[hd1]]).
cm_opts(n7, [add_cm_options=[r8(al)], add_pr_options=[depth_timeout(2)]]).
cm_opts(n8, [cm_cfg=std, add_cm_options=[hs]-[hd1,r8(al)]]).
cm_opts(n9, [cm_cfg=std]).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%
%%%% Exporting an LP-Interpolation Entailment as a TPTP Problem
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Example calls:
%%%%
%%%% ?- ipform_as_tptp_problem(14-1, '/tmp/test1.p', []).
%%%% ?- ipform_as_tptp_problem(14-5, '/tmp/test2.p', [lpip_simp_input=1]).
%%%% $ vampire /tmp/test2.p
%%%% $ eprover /tmp/test2.p
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ipform_as_tptp_problem(L, File, Opts) :-
exdef(L, P, Q, V),
p_def(P, Q, V, _, [lpip_dry=Form | Opts]),
ppl_valid(Form, [prover=tptp(none), file=File, printing=false]).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Verifying Non-Definability with Mace4
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Example call:
%%%%
%%%% exdef(14-1, P, Q, _), !, p_nondef(P, Q, [p], []).
%%%%
p_nondef(P, Q, V, Opts) :-
p_def(P, Q, V, _, [lpip_dry=Form|Opts]),
%% r=Result, where Result is unified with true (proven), false
%% (countermodel) or unknown:
ppl_valid(Form, [r=false, printing=false | Opts]).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Decoding Examples: Examples 10 and 11 in the Paper
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Run all decoding examples.
%%%%
ex_decode :-
( exform(Label, F),
ex_decode(F, Label, []),
fail
; true
),
( Label = 10-1,
exform(Label, F),
ex_decode(F, Label, [decode_partition=0]),
fail
; true
).
ex_decode(F, Label, Opts) :-
format('------------------------------------'),
format('------------------------------------~n'),
f_encodes_p_form(F, F1),
ppl_valid(F1, [r=Result, printing=false]),
( Result = true ->
format('Formula ~q decodes with options ~q to:~n',
[Label, Opts]),
f_decode_p(F, P, Opts),
pp(P),
nl
; Result = false ->
format('Formula ~q does not encode a program~n', [Label])
; format('Failed to prove that formula ~q encodes a program~n', [Label])
).
%%%%
%%%% Decoding examples.
%%%%
exform(10-1, ((~p0;q1;r0),
(~s1;t1;u1),
(~p1;q1;r1))).
exform(10-2, (~p1;q1;r0)).
exform(10-3, (~p0;q1;r0)).
exform(11, ((~p0;q1;r0),
(~p0;q1;r1),
(~p1;q1;r1))).
%%%%
%%%% Note: There are currently some simplifications in the sense of Remark 1
%%%% implemented (m_simp_msf_pos/2, m_simp_msf_lit/2) but none of these has
%%%% effect on example 11.
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Definability Examples: Examples 14 and 16 in the Paper
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Run all definability examples.
%%%%
ex_def :-
( exdef(Label, P, Q, V),
( exdef_special_options(Label, Opts) ->
true
; Opts = []
),
ex_def(P, Q, V, Label, Opts),
fail
; true
).
ex_def(P, Q, V, Label, Opts) :-
format('------------------------------------'),
format('------------------------------------~n'),
p_def(P, Q, V, R, Opts),
format('Found R for example ~q:~n', [Label]),
pp(R),
nl.
%%%%
%%%% Definability Examples
%%%%
%%%% Notes: In the automatically found result of Example 14-7 one rule is
%%%% expressed differently from the paper, but both versions are strongly
%%%% equivalent . In Examples 16-1 and 16-2 there is one rule in the result
%%%% that is redundant given P. The currently implemented simplifications do
%%%% not remove it.
%%%%
exdef_special_options(14-5, [lpip_simp_input=1]).
exdef_special_options(14-6, [pr_options=[d(1)]]).
exdef(14-1, P, Q, V) :-
P = [],
Q = [(p <-- q, r),
(p ; q <-- r),
(q <-- q, s)],
V = [p, r].
exdef(14-2, P, Q, V) :-
P = [p(X) <-- q(X)],
Q = [(r(X) <-- p(X)),
(r(X) <-- q(X))],
V = [p, r].
exdef(14-3, P, Q, V) :-
P = [(false <-- p(X), q(X))],
Q = [(r(X) <-- p(X), not q(X))],
V = [p, r].
exdef(14-4, P, Q, V) :-
P = [(p(X) <-- q(X), not r(X)),
(p(X) <-- s(X)),
(not r(X) ; s(X) <-- p(X)),
(q(X) ; s(X) <-- p(X))],
Q = [(t(X) <-- p(X))],
V = [q, r, s, t].
exdef(14-5, P, Q, V) :-
P = [(p(X) <-- q(X), not r(X)),
(p(X) <-- s(X)),
(not r(X) ; s(X) <-- p(X)),
(q(X) ; s(X) <-- p(X))],
Q = [(t(X) <-- s(X)),
(t(X) <-- q(X), not r(X))],
V = [p, t].
exdef(14-6, P, Q, V) :-
P = [(n(X) <-- z(X)),
(n(X) <-- n(Y), s(Y,X))],
Q = [(not n(X) <-- z(X0), s(X0,X1), s(X1,X))],
V = [s, z].
exdef(14-7, P, Q, V) :-
P = [(c(X,Y,Z) <-- r(X,Y), r(Y,Z)),
(false <-- c(X,Y,Z), not r(X,Y)),
(false <-- c(X,Y,Z), not r(Y,Z))],
Q = [(r(X,Y) ; not r(X,Y) <-- true),
(false <-- c(X,Y,Z), not r(X, Z))],
V = [r].
exdef(16-1, P, Q, V) :-
P = [(p <-- q)],
Q = [(r <-- p),
(r <-- q),
(q <-- s)],
V = v([p,q,r,s],[],[p,r,s]).
exdef(16-2, P, Q, V) :-
P = [(p <-- q)],
Q = [(false <-- q, not p),
(r <-- q),
(s <-- p)],
V = v([q,r,s],[],[p,q,r,s]).
exdef(16-3, P, Q, V) :-
P = [(p <-- q),
(r <-- p)],
Q = [(s <-- not r),
(r <-- q)],
V = v([s],[r],[p,q,r,s]).