17:- assert(proof(readable)). 18
19
21
22leancop_proof(Mat,Proof) :-
23 proof(compact) -> leancop_compact_proof(Proof) ;
24 proof(connect) -> leancop_connect_proof(Mat,Proof) ;
25 leancop_readable_proof(Mat,Proof).
26
28
29leancop_readable_proof(Mat,Proof) :-
30 print('------------------------------------------------------'),
31 nl,
32 print_explanations,
33 print('Proof:'), nl, print('------'), nl, nl,
34 print('Translation into (disjunctive) clausal form:'), nl,
35 print_clauses(Mat,1,Mat1),
36 print_introduction,
37 calc_proof(Mat1,Proof,Proof1),
38 print_proof(Proof1), nl,
39 print_ending,
40 print('------------------------------------------------------'),
41 nl.
42
44
45leancop_compact_proof(Proof) :-
46 print('------------------------------------------------------'),
47 nl,
48 print('Compact Proof:'), nl,
49 print('--------------'), nl,
50 print(Proof), nl,
51 print('------------------------------------------------------'),
52 nl.
53
55
56leancop_connect_proof(Mat,Proof) :-
57 print('------------------------------------------------------'),
58 nl,
59 print('Proof for the following clauses:'), nl,
60 print_clauses(Mat,1,Mat1),
61 calc_proof(Mat1,Proof,Proof1),
62 print('Connection Proof:'), nl,
63 print('-----------------'), nl,
64 print_connect_proof(Proof1),
65 print('------------------------------------------------------'),
66 nl.
67
68print_connect_proof([(Cla,Num,Sub)|Proof]) :-
69 print_connect_proof_step([],Cla,Num,Sub),
70 print_connect_proof(Proof,[1]).
71
72print_connect_proof([],_).
73
74print_connect_proof([[(Cla,Num,Sub)|Proof]|Proof2],[I|J]) :-
75 print_connect_proof_step([I|J],Cla,Num,Sub),
76 print_connect_proof(Proof,[1,I|J]), I1 is I+1,
77 print_connect_proof(Proof2,[I1|J]).
78
79print_connect_proof_step(I,Cla,Num,Sub) :-
80 append(I,[1],I1), print_step(I1), print(' '), print(Cla),
81 ( Num=(R:N) -> append(_,[H|T],I1), N1 is N+1, length([H|T],N1),
82 ( R=r -> print(' (reduction:'), print_step(T) ;
83 print(' (lemmata:'), print_step(T) ) ;
84 print(' ('), print(Num) ), print(') '),
85 ( Sub=[[],_] -> true ; print('substitution:'), print(Sub) ), nl.
86
87
89
90calc_proof(Mat,[Cla|Proof],[(Cla1,Num,Sub)|Proof1]) :-
91 ((Cla=[#|Cla1];Cla=[-!|Cla1]) -> true ; Cla1=Cla),
92 clause_num_sub(Cla1,[],[],Mat,1,Num,Sub),
93 calc_proof(Cla1,[],[],Mat,Proof,Proof1).
94
95calc_proof(_,_,_,_,[],[]).
96
97calc_proof(Cla,Path,Lem,Mat,[[Cla1|Proof]|Proof2],Proof1) :-
98 append(Cla2,[#|Cla3],Cla1), !, append(Cla2,Cla3,Cla4),
99 append(Pro1,[[[-(#)]]|Pro2],Proof), append(Pro1,Pro2,Proof3),
100 calc_proof(Cla,Path,Lem,Mat,[[Cla4|Proof3]|Proof2],Proof1).
101
102calc_proof([Lit|Cla],Path,Lem,Mat,[[Cla1|Proof]|Proof2],Proof1) :-
103 (-NegLit=Lit;-Lit=NegLit), append(Cla2,[NegL|Cla3],Cla1),
104 NegLit==NegL, append(Cla2,Cla3,Cla4), length([_|Path],I) ->
105 clause_num_sub(Cla1,Path,Lem,Mat,1,Num,Sub),
106 Proof1=[[([NegLit|Cla4],Num,Sub)|Proof3]|Proof4],
107 calc_proof(Cla4,[I:Lit|Path],Lem,Mat,Proof,Proof3),
108 (Lem=[I:J:_|_] -> J1 is J+1 ; J1=1),
109 calc_proof(Cla,Path,[I:J1:Lit|Lem],Mat,Proof2,Proof4).
110
112
113clause_num_sub([NegLit],Path,Lem,[],_,R:Num,[[],[]]) :-
114 (-NegLit=Lit;-Lit=NegLit), member(Num:J:LitL,Lem), LitL==Lit ->
115 R=J ; member(Num:NegL,Path), NegL==NegLit -> R=r.
116
117clause_num_sub(Cla,Path,Lem,[Cla1|Mat],I,Num,Sub) :-
118 append(Cla2,[L|Cla3],Cla1), append([L|Cla2],Cla3,Cla4),
119 instance1(Cla,Cla4) ->
120 Num=I, term_variables(Cla4,Var), copy_term(Cla4,Cla5),
121 term_variables(Cla5,Var1), Cla=Cla5, Sub=[Var,Var1] ;
122 I1 is I+1, clause_num_sub(Cla,Path,Lem,Mat,I1,Num,Sub).
123
124instance1(A,B) :-
125 \+ \+ (term_variables(A,VA), unify_with_occurs_check(A,B),
126 term_variables(A,VB), VA==VB).
127
129
130print_proof([(Cla,Num,Sub)|Proof]) :-
131 print_clause([],Cla,Num,Sub),
132 print_proof(Proof,[1]).
133
134print_proof([],_).
135
136print_proof([[(Cla,Num,Sub)|Proof]|Proof2],[I|J]) :-
137 print_proof_step([I|J],Cla,Num,Sub),
138 print_proof(Proof,[1,I|J]), I1 is I+1,
139 print_proof(Proof2,[I1|J]).
140
142
143print_proof_step(I,[Lit|Cla],Num,Sub) :-
144 print_assume(I,Lit),
145 ( Num=(R:N) -> append(_,[H|T],I), length([H|T],N),
146 (R=r -> print_redu(I,[H|T]) ; print_fact(I,[R|T])) ;
147 print_clause(I,Cla,Num,Sub) ).
148
149print_assume(I,Lit) :-
150 print_step(I), print(' Assume '), (-NegLit=Lit;-Lit=NegLit) ->
151 print(NegLit), print(' is '), print('false.'), nl.
152
153print_clause(I,Cla,Num,Sub) :-
154 print_sp(I), print(' Then clause ('), print(Num), print(')'),
155 ( Sub=[[],[]] -> true ; print(' under the substitution '),
156 print(Sub), nl, print_sp(I) ),
157 ( Cla=[] -> print(' is true.') ;
158 print(' is false if at least one of the following is false:'),
159 nl, print_sp(I), print(' '), print(Cla) ), nl.
160
161print_redu(I,J) :-
162 print_sp(I), print(' This is a contradiction to assumption '),
163 print_step(J), print('.'), nl.
164
165print_fact(I,J) :-
166 print_sp(I), print(' This assumption has been refuted in '),
167 print_step(J), print('.'), nl.
168
170
171print_clauses([],_,[]) :- nl.
172print_clauses([[-(#)]|Mat],I,Mat1) :- !, print_clauses(Mat,I,Mat1).
173print_clauses([Cla|Mat],I,Mat1) :-
174 append(Cla2,[#|Cla3],Cla), append(Cla2,Cla3,Cla1),
175 print_clauses([Cla1|Mat],I,Mat1).
176print_clauses([Cla|Mat],I,[Cla|Mat1]) :-
177 print(' ('), print(I), print(') '),
178 print(Cla), nl, I1 is I+1, print_clauses(Mat,I1,Mat1).
179
180print_step([I]) :- print(I).
181print_step([I,J|T]) :- print_step([J|T]), print('.'), print(I).
182
183print_sp([]).
184print_sp([I]) :- atom(I), !, print(' ').
185print_sp([I]) :- I<1.
186print_sp([I]) :- I>=1, print(' '), I1 is I/10, print_sp([I1]).
187print_sp([I,J|T]) :- print_sp([J|T]), print(' '), print_sp([I]).
188
190
191print_explanations :-
192 print('Explanations for the proof presented below:'), nl,
193 print('- to solve unsatisfiable problems they are negated'), nl,
194 print('- equality axioms are added if required'), nl,
195 print('- terms and variables are represented by Prolog terms'), nl,
196 print(' and Prolog variables, negation is represented by -'), nl,
197 print('- I^[t1,..,tn] represents the atom P_I(t1,..,tn)'), nl,
198 print(' or the Skolem term f_I(t1,t2,..,tn) introduced'), nl,
199 print(' during the clausal form translation'), nl,
200 print('- the substitution [[X1,..,Xn],[t1,..,tn]] represents'), nl,
201 print(' the assignments X1:=t1, .., Xn:=tn'), nl, nl.
202
203print_introduction :-
204 print('We prove that the given clauses are valid, i.e. for'), nl,
205 print('a given substitution they evaluate to true for all'), nl,
206 print('interpretations. The proof is by contradiction:'), nl,
207 print('Assume there is an interpretation so that the given'), nl,
208 print('clauses evaluate to false. Then in each clause there'), nl,
209 print('has to be at least one literal that is false.'), nl, nl.
210
211print_ending :-
212 print('Therefore there is no interpretation that makes all'), nl,
213 print('given clauses simultaneously false. Hence the given'), nl,
214 print('clauses are valid.'), nl,
215 print(' q.e.d.'), nl