%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% 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 .
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- module(synasp2, [p_gamma/2,
p_seq/3,
p_sentails/3,
f_encodes_p_form/2,
f_decode_p/3,
f_lp_ipol_form/4,
f_lp_ipol/4,
latest_ipol_form/1,
p_def/5,
p_interpolant/4
]).
/** 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
*/
:- use_module(folelim(logop_fol)).
:- use_module(folelim(prettysymbols_fol)).
:- use_module(folelim(utils_fol)).
:- use_module(folelim(simp_fol)).
:- use_module(folelim(innexing)).
:- use_module(nf(nf)).
:- use_module(swilib(err)).
%% For the syntax of logic programs:
:- op(900, fy, user:not).
:- op(1200, xfx, user:'<--').
%% true/false for empty body/head.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% The gamma Transformation
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
/** p_gamma(+Prog, -Form) is det.
Form is the gamma transformation of Prog.
*/
p_gamma(P, F) :-
findall(C, ( member(R, P),
gamma_0(R, C1),
( C = C1
; f_rename_01(C1, C)
)
),
Cs),
list_to_conjunction(Cs, F1),
uclose(F1, F).
gamma_0((H <-- B), C) :-
!,
gamma_0_h(H, CH),
gamma_0_b(B, CB),
logform_disjoin(CB, CH, C).
gamma_0(X, _) :-
err('Bad rule: ~q', [X]).
gamma_0_h(false, false) :-
!.
gamma_0_h((L ; H), (L1 ; H1)) :-
!,
plit_to_01(L, L1),
gamma_0_h(H, H1).
gamma_0_h(L, L1) :-
plit_to_01(L, L1).
gamma_0_b(true, false) :-
!.
gamma_0_b((L , H), (L1 ; H1)) :-
!,
plit_to_01(L, L2),
local_lit_complement(L2, L1),
gamma_0_b(H, H1).
gamma_0_b(L, L1) :-
plit_to_01(L, L2),
local_lit_complement(L2, L1).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
plit_to_01(not A, ~A1) :-
!,
A =.. [P|T],
atom_concat(P, '1', P1),
A1 =.. [P1|T].
plit_to_01(A, A1) :-
!,
A =.. [P|T],
atom_concat(P, '0', P1),
A1 =.. [P1|T].
plit_predicate(not A, P/N) :-
!,
functor(A, P, N).
plit_predicate(A, P/N) :-
functor(A, P, N).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
local_lit_atom(~A, A) :-
!.
local_lit_atom(A, A).
local_lit_complement(~A, A) :-
!.
local_lit_complement(A, ~A).
uclose(F, F1) :-
term_variables(F, V),
( V = [] ->
F1 = F
; logform_clean_vars_to_symbols(all(V, F), F2),
logform_vars_to_pretty_symbols(F2, F1)
).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
/** p_seq(+Prog1, +Prog2, +Options) is semidet.
Succeeds if it can be verified that Prog1 and Prog2 are strongly equivalent.
*/
p_seq(P, Q, Opts) :-
%% two implications are for most provers easier to handle than an
%% equivalence
p_seq_forms(P, Q, F1, F2),
ppl_valid(F1, [r=true, printing=false | Opts]),
info(9, 'Verified ->'),
ppl_valid(F2, [r=true, printing=false | Opts]),
info(9, 'Verified <-').
p_seq_forms(P, Q, F1, F2) :-
append(P, Q, PQ),
p_sub(PQ, S),
p_gamma(P, FP),
p_gamma(Q, FQ),
F1 = (S,FP -> FQ),
F2 = (S,FQ -> FP).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Decoding
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
/** f_encodes_p_form(+Form1, -Form2) is det.
Form2 is valid iff Form1 encodes a logic program.
*/
f_encodes_p_form(F, F1) :-
f_sub(F, S),
f_rename_01(F, R),
F1 = (F, S -> R).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
/** 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_decode_p(F, P, Opts) :-
( memberchk(decode_cnf=CNF, Opts) -> true ; CNF = 3 ),
( memberchk(decode_partition=PM, Opts) -> true ; PM = 1 ),
( memberchk(decode_simp=Simp, Opts) -> true ; Simp = 1 ),
( CNF = 0 ->
cnf_fewsimp(F, M)
; CNF = 1 ->
cnf(F, M)
; CNF = 3 ->
cnf6(F, M)
),
( Simp = 0 ->
MS = M
; Simp = 1 ->
m_simp_msf_1(M, MS)
; Simp = 2 ->
m_simp_msf_2(M, MS)
; Simp = 3 ->
m_simp_msf_3(M, MS)
),
m_split_01(MS, M0, M1),
( PM = 0 ->
M1_1 = M1
; PM = 1 ->
m_decode_partition(M1, M0, M1_1, _)
),
append(M0, M1_1, MP),
m_to_p(MP, P1),
align_vars(P1, _, P).
m_to_p(MP, P) :-
findall(R, ( member(C, MP), c_to_r(C, R) ), P).
c_to_r(C, (H <-- B)) :-
cr1(C, PH, NH, PB, NB),
append(PH, NH, H1),
list_to_disjunction(H1, H),
append(PB, NB, B1),
list_to_conjunction(B1, B).
cr1([~A|C], PH, NH, PB, NB) :-
!,
A =.. [P|T],
sub_atom(P, 0, _, 1, P1),
A1 =.. [P1|T],
( sub_atom(P, _, 1, 0, '0') ->
PB = [A1|PB1],
PH = PH1,
NH = NH1,
NB = NB1
; NH = [not A1|NH1],
PH = PH1,
PB = PB1,
NB = NB1
),
cr1(C, PH1, NH1, PB1, NB1).
cr1([A|C], PH, NH, PB, NB) :-
A =.. [P|T],
sub_atom(P, 0, _, 1, P1),
A1 =.. [P1|T],
( sub_atom(P, _, 1, 0, '0') ->
PH = [A1|PH1],
PB = PB1,
NH = NH1,
NB = NB1
; NB = [not A1|NB1],
PH = PH1,
NH = NH1,
PB = PB1
),
cr1(C, PH1, NH1, PB1, NB1).
cr1([], [], [], [], []).
align_vars([C|Cs], Vs, [C1|Cs1]) :-
copy_term(C, C1),
term_variables(C1, Vs1),
set_vars(Vs1, Vs),
align_vars(Cs, Vs, Cs1).
align_vars([], _, []).
set_vars([V|Vs], [V|Vs1]) :-
set_vars(Vs, Vs1).
set_vars([], _).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
m_decode_partition(M1, M0, M1_1, M1_2) :-
m_rename_01(M0, M00),
mdp(M1, M00, M1_1, M1_2).
mdp([C|M], M00, M1_1, M1_2) :-
( member(D, M00),
clause_subsumes_chk(D, C) ->
M1_2 = [C|M1_22],
M1_1 = M1_11
; M1_2 = M1_22,
M1_1 = [C|M1_11]
),
mdp(M, M00, M1_11, M1_22).
mdp([], _, [], []).
m_split_01([C|M], M0, M1) :-
( c_contains_0(C) ->
M0 = [C|M00],
M1 = M11
; M0 = M00,
M1 = [C|M11]
),
m_split_01(M, M00, M11).
m_split_01([], [], []).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c_contains_0(C) :-
member(L, C),
local_lit_atom(L, A),
functor(A, P, _),
sub_atom(P, _, 1, 0, '0').
c_is_taut(C) :-
member(~A, C),
member(B, C),
A == B,
!.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Renaming the "Superscript Decoration"
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f_rename_01(F, F1) :-
f_preds(F, Ps),
findall(P-P1, ( member(P, Ps), pred0_to_pred1(P, P1) ), Map),
logform_rename_free_predicates(F, Map, pn, F1).
m_rename_01(M, M1) :-
findall(C, ( member(C1, M),
c_rename_01(C1, C) ),
M1).
c_rename_01([L|Ls], [L1|Ls1]) :-
lit_rename_01(L, L1),
c_rename_01(Ls, Ls1).
c_rename_01([], []).
lit_rename_01(~A, ~A1) :-
!,
logatom_rename_01(A, A1).
lit_rename_01(A, A1) :-
logatom_rename_01(A, A1).
logatom_rename_01(A, A1) :-
A =.. [P|T],
pred0_to_pred1(P, P1),
!,
A1 =.. [P1|T].
logatom_rename_01(A, A).
logatom_rename_pos_10(A, A1) :-
A =.. [P|T],
pred1_to_pred0(P, P1),
!,
A1 =.. [P1|T].
logatom_rename_pos_10(A, A).
logatom_rename_neg_01(A, A1) :-
A =.. [P|T],
pred0_to_pred1(P, P1),
!,
A1 =.. [P1|T].
logatom_rename_neg_01(A, A).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Some Formula Simplifications that are Modulo "S_F", Preserving
%%%% Strong Equivalence
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
m_simp_msf_1(M, M1) :-
m_simp_msf_lit(M, M2),
m_simp_msf_pos(M2, M1).
m_simp_msf_2(M, M1) :-
m_simp_msf_pos(M, M1).
m_simp_msf_3(M, M1) :-
m_simp_msf_lit(M, M2),
m_simp_msf_pos(M2, M3),
m_simp_msf_neg(M3, M1).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Removal of a clause $C$ if, after setting in $C$ the superscript of all
%%%% positive literals to $0$, the clause is tautological or is subsumed by
%%%% some other clause~$D$.
%%%%
m_simp_msf_pos(M, M1) :-
select(C, M, M2),
c_rename_pos_10(C, C1),
( c_is_taut(C1) ->
true
; member(D, M2),
clause_subsumes_chk(D, C1)
),
!,
m_simp_msf_pos(M2, M1).
m_simp_msf_pos(M, M).
c_rename_pos_10([L|Ls], [L1|Ls1]) :-
lit_rename_pos_10(L, L1),
c_rename_pos_10(Ls, Ls1).
c_rename_pos_10([], []).
lit_rename_pos_10(~A, ~A) :-
!.
lit_rename_pos_10(A, A1) :-
logatom_rename_pos_10(A, A1).
%%%%
%%%% Analogous to m_simp_msf_pos. Not sure if m_simp_msf_neg is often
%%%% applicable.
%%%%
m_simp_msf_neg(M, M1) :-
select(C, M, M2),
c_rename_neg_01(C, C1),
( c_is_taut(C1) ->
true
; member(D, M2),
clause_subsumes_chk(D, C1)
),
!,
info(10, 'MSF NEG STEP PERFORMED'),
m_simp_msf_neg(M2, M1).
m_simp_msf_neg(M, M).
c_rename_neg_01([L|Ls], [L1|Ls1]) :-
lit_rename_neg_01(L, L1),
c_rename_neg_01(Ls, Ls1).
c_rename_neg_01([], []).
lit_rename_neg_01(~A, ~A1) :-
!,
logatom_rename_neg_01(A, A1).
lit_rename_neg_01(A, A).
%%%%
%%%% Removal of a positive (negative) literal superscripted with $0$ ($1$)
%%%% from a clause if a literal with the same polarity, same arguments and the
%%%% corresponding predicate superscripted with $1$ ($0$) is also in the
%%%% clause.
%%%%
m_simp_msf_lit(M, M1) :-
map_c_msm(M, M1).
map_c_msm([X|Xs], [X1|Xs1]) :-
c_msm(X, X, X1),
map_c_msm(Xs, Xs1).
map_c_msm([], []).
c_msm([~A|C], D, E) :-
a_msm_1(A, A0),
copy_term(A0, A0C),
member(~A0C, D),
A0C == A0,
!,
c_msm(C, D, E).
c_msm([~A|C], D, [~A|E]) :-
!,
c_msm(C, D, E).
c_msm([A|C], D, E) :-
a_msm_0(A, A1),
copy_term(A1, A1C),
member(A1C, D),
A1C == A1,
!,
c_msm(C, D, E).
c_msm([A|C], D, [A|E]) :-
!,
c_msm(C, D, E).
c_msm([], _, []).
a_msm_1(A, A0) :-
A =.. [P|T],
sub_atom(P, _, 1, 0, '1'),
!,
sub_atom(P, 0, _, 1, P1),
atom_concat(P1, '0', P2),
A0 =.. [P2|T].
a_msm_0(A, A0) :-
A =.. [P|T],
sub_atom(P, _, 1, 0, '0'),
!,
sub_atom(P, 0, _, 1, P1),
atom_concat(P1, '1', P2),
A0 =.. [P2|T].
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
pred1_to_pred0(P0, P1) :-
sub_atom(P0, _, 1, 0, '1'),
!,
sub_atom(P0, 0, _, 1, P),
atom_concat(P, '0', P1).
pred0_to_pred1(P0, P1) :-
sub_atom(P0, _, 1, 0, '0'),
!,
sub_atom(P0, 0, _, 1, P),
atom_concat(P, '1', P1).
pred01_to_pred(P01, P) :-
sub_atom(P01, _, 1, 0, X),
( X = '0' -> true ; X = '1' ),
!,
sub_atom(P01, 0, _, 1, P).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
p_predicates(Prog, PNs) :-
findall(P/N, ( member(R, Prog),
rule_predicate(R, P/N)
),
PNs1),
sort(PNs1, PNs).
rule_predicate((H <-- B), P/N) :-
( rule_predicate_h(H, P/N)
; rule_predicate_b(B, P/N)
).
rule_predicate_h((L ; H), P/N) :-
!,
( plit_predicate(L, P/N)
; rule_predicate_h(H, P/N)
).
rule_predicate_h(false, _) :-
!,
fail.
rule_predicate_h(L, P/N) :-
plit_predicate(L, P/N).
rule_predicate_b((L , B), P/N) :-
!,
( plit_predicate(L, P/N)
; rule_predicate_b(B, P/N)
).
rule_predicate_b(true, _) :-
!,
fail.
rule_predicate_b(L, P/N) :-
plit_predicate(L, P/N).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
p_sub(P, S) :-
p_predicates(P, PNs),
pns_sub(PNs, S).
f_sub(F, S) :-
f_signature(F, PNs, _),
findall(P/N, ( member(P1/N, PNs),
pred01_to_pred(P1, P) ),
PNs1),
sort(PNs1, PNs2),
pns_sub(PNs2, S).
pns_sub(PNs, S) :-
findall(F1, ( member(P/N, PNs),
pn_sub(P/N, F1) ),
Fs),
list_to_conjunction(Fs, S1),
f_join_quants(S1, S).
pn_sub(P/N, F) :-
atom_concat(P, '0', P0),
atom_concat(P, '1', P1),
functor(A0, P0, N),
functor(A1, P1, N),
A0 =.. [_|T],
A1 =.. [_|T],
( T = [] ->
F = (~A0 ; A1)
; uclose((~A0 ; A1), F)
).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% LP-Interpolation
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
/** 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.
*/
f_lp_ipol_form(F, G, Opts, F1) :-
f_sub(F, SF),
f_sub(G, SG),
( memberchk(lpip_simp_input = LSI, Opts) -> true ; LSI = 0 ),
( LSI = 1 ->
F2 = F,
f_join_quants(G, G2)
; LSI = 2 ->
f_join_quants(F, F2),
f_join_quants(G, G2)
; F2 = F,
G2 = G
),
logform_conjoin(F2, SF, Left),
logform_negate(SG, SGN),
logform_disjoin(SGN, G2, Right),
F1 = (Left -> Right).
/** 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.
*/
:- dynamic latest_ipol_form/1.
/** 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.
*/
f_lp_ipol(F, G, H, Opts) :-
f_lp_ipol_form(F, G, Opts, F1),
retractall( latest_ipol_form(_) ),
asserta( latest_ipol_form(F1) ),
( memberchk(lpip_dry=F1, Opts) ->
true
; ppl_ipol(F1, [r=H0, printing=false|Opts]),
f_rename_01(H0, H1),
logform_conjoin(H0, H1, H),
( memberchk(lpip_h=H, Opts) -> true ; true )
).
%% Some possible options for interpolation:
%% [ip_mode=hyper] (for cmprover)
%% [prover=prover9]
%% [enum_ips=3,add_cm_options=[]-[r8(_)]]
%% [add_cm_options=[ordp]]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Synthesis
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
/** 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.
@arg 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.
@arg 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_def(P, Q, V, R, Opts) :-
( memberchk(formpreds, Opts) ->
V1 = V
; V = v(_,_,_) ->
( memberchk(forget, Opts) ->
v3preds_for_forgetting(V, V1)
; v3preds(V, V1)
)
; findall(P1, ( member(P2, V),
( atom_concat(P2, '0', P1)
; atom_concat(P2, '1', P1)
)
),
V2),
sort(V2, V1)
),
p_gamma(P, FP),
p_gamma(Q, FQ),
logform_conjoin(FP, FQ, Left1),
logform_negate(FP, FPN),
logform_disjoin(FPN, FQ, Right0),
( memberchk(forget, Opts) ->
f_prime(Right0, V1, Right1)
; f_prime_except(Right0, V1, Right1)
),
( memberchk(lpdef_dry=(Left1-Right1), Opts) ->
true
; f_lp_ipol(Left1, Right1, H, Opts),
( memberchk(lpip_dry=_, Opts) ->
true
; f_decode_p(H, R, Opts)
)
).
v3preds(v(V1,V2,V3), V) :-
%% Here we handle V1,V2 auch that:
%% allowed in pos head = V1
%% allowed in neg body = V1 cup V2
findall(P-Pol, ( member(P1, V1), atom_concat(P1, '0', P), Pol = p
; member(P1, V1), atom_concat(P1, '1', P), Pol = p
; member(P1, V2), atom_concat(P1, '1', P), Pol = p
; member(P1, V3), atom_concat(P1, '0', P), Pol = n
; member(P1, V3), atom_concat(P1, '1', P), Pol = n
),
V0),
sort(V0, V).
v3preds_for_forgetting(v(V1,V2,V3), V) :-
%% Here we handle V1,V2 auch that:
%% not allowed in pos head = V1 cup V2
%% not allowed in neg body = V2
findall(P-Pol, ( member(P1, V1), atom_concat(P1, '0', P), Pol = p
; member(P1, V2), atom_concat(P1, '0', P), Pol = p
; member(P1, V2), atom_concat(P1, '1', P), Pol = p
; member(P1, V3), atom_concat(P1, '0', P), Pol = n
; member(P1, V3), atom_concat(P1, '1', P), Pol = n
),
V0),
sort(V0, V).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f_preds(F, Ps) :-
findall(P,
(logform_enum_atoms(F, A), functor(A, P, _)),
Ps1),
sort(Ps1, Ps).
f_predpols(F, PPs) :-
findall(P-Pol,
(logform_enum_atoms(F, A, Pol), functor(A, P, _)),
PPs1),
sort(PPs1, PPs).
f_predpols_allpols(F, Ps) :-
findall(P-Pol,
(logform_enum_atoms(F, A), functor(A, P, _),
(Pol = p ; Pol = n)),
Ps1),
sort(Ps1, Ps).
f_predpols_n(F, PPs) :-
findall((P/N)-Pol,
(logform_enum_atoms(F, A, Pol), functor(A, P, N)), PPs1),
sort(PPs1, PPs).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
canonicalize_predpols(PPs, PPs1) :-
findall(P-Pol, ( member(X, PPs),
( atom(X) ->
P = X,
( Pol = p ; Pol = n)
; X = P-Pol1,
( Pol1 = pn ->
( Pol = p ; Pol = n)
; Pol = Pol1
)
)
),
PPs2),
sort(PPs2, PPs1).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% The objective of this simplification is to keep the number of distinct
%%%% variables small. In particular to obtain a small number of distinct
%%%% Skolem terms with conventional Skolemization methods, which can have a
%%%% big effect on provers (CMProver) and the size of resulting proofs
%%%% (Prover9). Also to let formulas without Skolemized variables look nicer.
%%%% It is for now a bit ad-hoc and should be replaced by something more
%%%% systematic. Maybe there are related known Skolemization techniques. Maybe
%%%% it is required in two versions for positve and negative polarity of the
%%%% input formulas, to prevent moving existential over universal quantifiers,
%%%% or vice versa, which would result in Skolem functions with unnecessary
%%%% many arguments.
%%%%
f_join_quants(F, F1) :-
quants_inward(F, F2),
f_merge_quants(F2, F1).
f_merge_quants(F, F1) :-
logform_clean_vars_to_prolog_vars(F, F2),
logform_process_subforms(F2, fmq_aux, F3),
logform_clean_vars_to_symbols(F3, F4),
logform_vars_to_pretty_symbols(F4, F1).
fmq_aux((all(X, F), all(Y, G)), all(Z, FG)) :-
!,
fmq_merge_quants(X, Y, Z),
logform_conjoin(F, G, FG).
fmq_aux((ex(X, F); ex(Y, G)), ex(Z, FG)) :-
!,
fmq_merge_quants(X, Y, Z),
logform_disjoin(F, G, FG).
% fmq_aux((all(X, F), G), all(X, FG)) :-
% !,
% logform_conjoin(F, G, FG).
% fmq_aux((F, all(X, G)), all(X, FG)) :-
% !,
% logform_conjoin(F, G, FG).
% fmq_aux((all(X, F) ; G), all(X, FG)) :-
% !,
% logform_disjoin(F, G, FG).
% fmq_aux((F ; all(X, G)), all(X, FG)) :-
% !,
% logform_disjoin(F, G, FG).
% fmq_aux((ex(X, F); G), ex(X, FG)) :-
% !,
% logform_disjoin(F, G, FG).
% fmq_aux((F; ex(X, G)), ex(X, FG)) :-
% !,
% logform_disjoin(F, G, FG).
% fmq_aux((ex(X, F), G), ex(X, FG)) :-
% !,
% logform_conjoin(F, G, FG).
% fmq_aux((F, ex(X, G)), ex(X, FG)) :-
% !,
% logform_conjoin(F, G, FG).
fmq_aux(X, X).
fmq_merge_quants(X, Y, Z) :-
var(X),
!,
fmq_merge_quants([X], Y, Z).
fmq_merge_quants(X, Y, Z) :-
var(Y),
!,
fmq_merge_quants(X, [Y], Z).
fmq_merge_quants([X|Xs], [Y|Ys], [X|Zs]) :-
!,
X = Y,
fmq_merge_quants(Xs, Ys, Zs).
fmq_merge_quants([], Y, Y) :-
!.
fmq_merge_quants(X, [], X).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Priming
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f_prime(F, PPs, F1) :-
canonicalize_predpols(PPs, PPs1),
f_predpols(F, PPF),
ord_intersect(PPF, PPs1, PPE),
findall(P, member(P-p, PPE), PEPos),
findall(P, member(P-n, PPE), PENeg),
ord_intersect(PEPos, PENeg, PEBoth),
ord_subtract(PEPos, PENeg, PEOnlyPos),
ord_subtract(PENeg, PEPos, PEOnlyNeg),
findall(P, member(P-p, PPF), PFPos),
findall(P, member(P-n, PPF), PFNeg),
ord_intersect(PEOnlyPos, PFNeg, PEAuxPos),
ord_intersect(PEOnlyNeg, PFPos, PEAuxNeg),
ord_subtract(PEOnlyPos, PFNeg, PETVPos),
ord_subtract(PEOnlyNeg, PFPos, PETVNeg),
info(10, 'B: ~q P: ~q N: ~q PTV: ~q NTV: ~q',
[PEBoth, PEAuxPos, PEAuxNeg, PETVPos, PETVNeg]),
findall(P-Prime, ( ( member(P, PEBoth)
; member(P, PEAuxPos)
; member(P, PEAuxNeg)
),
prime_predicate(P, Prime) ),
Map),
logform_rename_free_predicates(F, Map, pn, F2),
f_replace_predicates_by_tv(F2, PETVPos, false, F3),
f_replace_predicates_by_tv(F3, PETVNeg, true, F4),
f_signature(F, PNs, _),
findall(P/N, (member(P, PEAuxPos), memberchk(P/N, PNs)), PNPos),
findall(P/N, (member(P, PEAuxNeg), memberchk(P/N, PNs)), PNNeg),
prime_aux_forms(PNNeg, FXP, p),
prime_aux_forms(PNPos, FXN, n),
logform_conjoin(FXP, FXN, FX),
( FX == true ->
F5 = F4
; logform_disjoin(F4, ~FX, F5)
),
simp_fol_fast(F5, F1).
f_prime_except(F, PPs, F1) :-
canonicalize_predpols(PPs, PPs1),
f_predpols(F, PPs2),
ord_subtract(PPs2, PPs1, PPs3),
f_prime(F, PPs3, F1).
f_replace_predicates_by_tv(F, Preds, TV, F1) :-
logform_process_subforms(F, rptv_aux(Preds, TV), F1).
rptv_aux(Preds, TV, F, F1) :-
logform_is_atom(F),
functor(F, Pred, _),
memberchk(Pred, Preds),
!,
F1 = TV.
rptv_aux(_, _, F, F).
prime_aux_forms(PNs, F, Mode) :-
findall(F1, ( member(P/N, PNs),
prime_predicate(P, PPrime),
functor(A, P, N),
A =.. [_|T],
B =.. [PPrime|T],
( Mode = p -> (F2 = (A->B))
; Mode = n -> (F2 = (B->A))
),
uclose(F2, F1) ),
Fs),
list_to_conjunction(Fs, F).
prime_predicate(P, PPrime) :-
sub_atom(P, _, 1, 0, PDeco),
( PDeco = '0' -> true ; PDeco = '1' ),
!,
sub_atom(P, 0, _, 1, PPure),
atomic_list_concat([PPure, '_prime_', PDeco], PPrime).
prime_predicate(P, PPrime) :-
atom_concat(P, '_prime', PPrime).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Interpolation Between Logic Programs, Based on Strong Equivalence
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
/** 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_sentails(P, Q, Opts) :-
( memberchk(v1, Opts) ->
p_sentails_v1(P, Q, Opts)
; p_sentails_v2(P, Q, Opts)
).
p_sentails_v1(P, Q, Opts) :-
p_sub(P, SP),
p_sub(Q, SQ),
p_gamma(P, FP),
p_gamma(Q, FQ),
Form = ((SP, FP) -> (~SQ;FQ)),
asserta(fff(Form)),
ppl_valid(Form, [r=true, printing=false | Opts]).
p_sentails_v2(P, Q, Opts) :-
p_gamma(P, FP),
p_gamma(Q, FQ),
f_lp_ipol_form(FP, FQ, Opts, Form),
ppl_valid(Form, [r=true, printing=false | Opts]).
/** 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.
*/
p_interpolant(P, Q, R, Opts) :-
p_gamma(P, FP),
p_gamma(Q, FQ),
f_lp_ipol_form(FP, FQ, Opts, F1),
retractall( latest_ipol_form(_) ),
asserta( latest_ipol_form(F1) ),
( memberchk(lpip_dry=F1, Opts) ->
true
; ppl_ipol(F1, [r=H0, printing=false|Opts]),
f_rename_01(H0, H1),
logform_conjoin(H0, H1, H),
( memberchk(lpip_h=H, Opts) -> true ; true )
),
f_decode_p(H, R, Opts).