1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2%
3% Copyright 2003-2010, Renate Schmidt,  University of Manchester
4%           2009-2010, Ullrich Hustadt, University of Liverpool
5%
6%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7
8prove(Fml, Result) :-
9    provable([], Fml, Result).
10
11provable(Fml, Result) :-
12    provable([], Fml, Result).
13
14provable(Axioms, FmlInput, unprovable) :-
15    retractall(consistent(_,_,_)),
16    retractall(inconsistent(_)),
17    retractall(reduced(_,_,_)),
18    % Axioms is a set of non-logical axioms, i.e. a background theory
19    create_search_output_file,
20
21    negated_formula(FmlInput, Fml),
22
23    nl,
24    pdl_write('** Input: '), pdl_write(Fml), pdl_nl,
25
26    % Transform Axioms and Fml into negation normal form
27    pdl_write('** NFAxioms:   '), pdl_nl,
28    normalise(Axioms, NFAxioms),
29    normalise(Fml, [], NFFml, Paths),
30
31    pdl_write('** NFFml:   '), pdl_write(NFFml), pdl_nl,
32    pdl_write('Paths = '), pdl_write(Paths), pdl_nl,
33
34    (get_output_format(latex) ->
35         latex_output(begin)
36         ;
37         true),
38
39    % Search for a proof or a model
40    search(NFAxioms, NFFml), !,
41
42    (get_output_format(latex) ->
43         latex_output(end)
44         ;
45         true).
46
47provable(_, _, provable) :-
48    print_result('Refutation proof found'),
49    (get_output_format(latex) ->
50         latex_output(end)
51         ;
52         true).
53
54%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
55
56satisfiable(Fml, Result) :-
57    satisfiable([], Fml, Result).
58
59satisfiable(Axioms, FmlInput, satisfiable) :-
60    retractall(consistent(_,_,_)),
61    retractall(inconsistent(_)),
62    % Axioms is a set of non-logical axioms, i.e. a background theory
63    create_search_output_file,
64
65    FmlInput = Fml,
66
67    nl,
68    pdl_write('** Input: '), pdl_write(Fml), pdl_nl,
69
70    % Transform Axioms and Fml into negation normal form
71    pdl_write('** NFAxioms:   '), pdl_nl,
72    normalise(Axioms, NFAxioms),
73    normalise(Fml, [], NFFml, Paths),
74
75    pdl_write('** NFFml:   '), pdl_write(NFFml), pdl_nl,
76    pdl_write('Paths = '), pdl_write(Paths), pdl_nl,
77
78    (get_output_format(latex) ->
79         latex_output(begin)
80         ;
81         true),
82
83    % Search for a proof or a model
84    search(NFAxioms, NFFml), !,
85
86    (get_output_format(latex) ->
87         latex_output(end)
88         ;
89         true).
90
91satisfiable(_, _, unsatisfiable) :-
92    print_result('Refutation found'),
93    (get_output_format(latex) ->
94         latex_output(end)
95         ;
96         true).
97
98%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
99
100negated_formula(Fml, not(Fml)) :-
101    get_negate_first(yes), !.
102
103negated_formula(Fml, Fml).
104
105%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
106%
107% search(+Axioms, +Formula)
108%
109%     Formula is a term including the formula to be tested for
110%     satisfiability and encodings of the positions of all subformulae
111%     The formula is in negation normal form.
112
113search(Axioms, Fml) :-
114    set_satisfiable_flag(-1),
115    set_states_counter(0),
116    set_proof_steps_counter(-1),
117    set_branch_point_counter(0),
118    set_sat_reuse_counter(0),
119    set_unsat_reuse_counter(0),
120
121    print_proof_step(0, Axioms, '[theory]'),
122    print_proof_step(0, Fml, '[given]'),
123
124    search_state(Axioms, [Fml], 0, [], NewBranch, [], NewEventualities, [], _),
125    pdl_write('In search, State : '), pdl_write(0), pdl_nl,
126    pdl_write('    Axioms : '),       pdl_write(Axioms), pdl_nl,
127    pdl_write('    NewBranch : '),    pdl_write(NewBranch), pdl_nl,
128    pdl_write('    NewEventualities : '), pdl_write(NewEventualities), pdl_nl,
129    test_ignorability(NewBranch, NewEventualities),
130%    write('Remembering consistent set - state shown consistent'), write(FmlList), nl,
131%    print_proof_step(State, consistent_set(FmlList), '[consistent set]'),
132%    store_consistent(FmlList,Branch,NewBranch,Eventualities,NewEventualities)
133    print_result('Satisfiable branch found').
134
135%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
136%
137% search_state(+Axioms, +Unexpanded, +State, +Branch, -NewBranch,
138%              +Eventualities, -NewEventualities)
139%
140%   Test whether a model for < State : Unexpanded > can be constructed.
141%   The formulae in Unexpanded are assumed to be in negation normal form.
142%   * +Branch is the branch constructed so far (i.e. the segment from the
143%     root state/world to the parent state/world of +State)
144%   * -NewBranch will be a \pi-completed branch extending +Branch
145%   * +Eventualities will be the eventualities fulfilled so far on +Branch
146%   * -NewEventualities will be eventualities fulfilled on -NewBranch
147%   Note: The predicate search_state is also used in reduce_existentials.
148
149search_state(Axioms, Unexpanded, State, Branch, NewBranch,
150        Eventualities, NewEventualities, IDT, ODT) :-
151    pdl_write('In search_state, State : '), pdl_write(State),  pdl_nl,
152    pdl_write('    Unexpanded : '),         pdl_write(Branch), pdl_nl,
153
154    print_proof_step(State, Axioms, '[theory-inst]'),
155    append(Unexpanded, Axioms, UnexpandedPlusAxioms),
156    % Remember: +LocalEventualities in the following call to reduce_local are
157    % the eventualities fulfilled in the current state +State
158    reduce_local(UnexpandedPlusAxioms, State, [], Workedoff,
159                 Universal, Existential, LocalEventualities, IDT, ODT_RL),
160
161    eliminate_duplicates(Workedoff, SimplifiedWorkedoff),
162    eliminate_duplicates(Universal, SimplifiedUniversal),
163    eliminate_duplicates(Existential, SimplifiedExistential),
164
165    pdl_write('    Branch : '), pdl_write(Branch), pdl_nl,
166    pdl_write('    SimplifiedWorkedoff : '), pdl_write(SimplifiedWorkedoff), pdl_nl,
167    pdl_write('    SimplifiedUniversal : '), pdl_write(SimplifiedUniversal), pdl_nl,
168    pdl_write('    SimplifiedExistential : '), pdl_write(SimplifiedExistential), pdl_nl,
169    pdl_write('    LocalEventualities : '), pdl_write(LocalEventualities), pdl_nl,
170
171    test_unsatisfiability(State, SimplifiedWorkedoff, SimplifiedWorkedoff),
172
173    merge_set(SimplifiedWorkedoff, SimplifiedExistential, Aux),
174    merge_set(Aux, SimplifiedUniversal, FmlList),
175
176    pdl_write('    FmlList : '), pdl_write(FmlList), pdl_nl,
177
178    prefix_to_list(State,StateList),
179    assert(reduced(ODT_RL, StateList, FmlList)),
180    (known_consistent(FmlList,BranchForFmlList,EventualitiesForFmlList) ->
181	pdl_write('    is known to be consistent'), pdl_nl,
182	append(BranchForFmlList,Branch,NewBranch),
183	append(EventualitiesForFmlList,Eventualities,NewEventualities)
184    ;
185	extend_branch(State, FmlList, Branch, ExtendedBranch),
186	pdl_write('    ExtendedBranch : '), pdl_write(ExtendedBranch), pdl_nl,
187
188	merge_set(Eventualities, LocalEventualities, ExtendedEventualities),
189	pdl_write('    ExtendedEventualities : '), pdl_write(ExtendedEventualities), pdl_nl,
190
191	search_state_aux(Axioms, SimplifiedExistential,
192                         SimplifiedUniversal, Unexpanded, State, ExtendedBranch, NewBranch,
193                         ExtendedEventualities, NewEventualities, ODT_RL, ODT)
194    ).
195
196%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
197
198% 4th argument not used.
199search_state_aux(_, _, _, _, State,
200            [pr(State,FmlList)|Branch], [EqualStates,pr(State,FmlList)|Branch],
201            ExtendedEventualities, ExtendedEventualities, IDT, IDT) :-
202    pdl_write_ln('In search_state_aux (1)....'),
203    pdl_write('    State : '),   pdl_write(State),   pdl_nl,
204    pdl_write('    FmlList : '), pdl_write(FmlList), pdl_nl,
205    pdl_write('    Branch : '),  pdl_write(Branch),  pdl_nl,
206    is_copy(FmlList, State, Branch, EqualStates), !.
207
208search_state_aux(Axioms, SimplifiedExistential, SimplifiedUniversal,
209            _, State, ExtendedBranch, NewBranch,
210            ExtendedEventualities, NewEventualities, IDT, ODT) :-
211%   pdl_write_ln('In search_state_aux (2)....'),
212    reduce_existentials(Axioms, SimplifiedExistential, State,
213                       SimplifiedUniversal, ExtendedBranch, NewBranch,
214                       ExtendedEventualities, NewEventualities, IDT, ODT).
215
216%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
217%
218% extend_branch(+State, +FmlList, +Branch, -ExtendedBranch)
219
220extend_branch(State, FmlList, Branch, [pr(State, FmlList)|Branch]).
221
222%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
223%
224%    The key proof_steps_counter counts the proof steps
225
226set_proof_steps_counter(Number) :- !,
227    pdl_write('set_proof_steps_counter to '), pdl_write(Number), pdl_nl,
228    flag(proof_steps_counter, _, Number).
229
230increment_proof_steps_counter(Increment) :- !,
231    flag(proof_steps_counter, Old, Old + Increment).
232
233get_proof_steps_counter(Number) :- !,
234    flag(proof_steps_counter, Number, Number).
235
236%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
237%
238%    The key states_counter counts the states created
239
240set_states_counter(Number) :- !,
241    pdl_write('set_states_counter to '), pdl_write(Number), pdl_nl,
242    flag(states_counter, _, Number).
243
244increment_states_counter(Increment) :- !,
245    flag(states_counter, Old, Old + Increment).
246
247get_states_counter(Number) :- !,
248    flag(states_counter, Number, Number).
249
250%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
251%
252%    The key branch_point_counter counts the branch_points
253
254set_branch_point_counter(Number) :- !,
255    pdl_write('set_branch_point_counter to '), pdl_write(Number), pdl_nl,
256    flag(branch_point_counter, _, Number).
257
258increment_branch_point_counter(Increment) :- !,
259    flag(branch_point_counter, Old, Old + Increment).
260
261get_branch_point_counter(Number) :- !,
262    flag(branch_point_counter, Number, Number).
263
264%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
265%
266%    The key sat_reuse_counter counts the number of times a stored
267%    satisfiable set is re-used
268
269set_sat_reuse_counter(Number) :- !,
270    pdl_write('set_sat_reuse_counter to '), pdl_write(Number), pdl_nl,
271    flag(sat_reuse_counter, _, Number).
272
273increment_sat_reuse_counter(Increment) :- !,
274    flag(sat_reuse_counter, Old, Old + Increment).
275
276get_sat_reuse_counter(Number) :- !,
277    flag(sat_reuse_counter, Number, Number).
278
279%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
280%
281%    The key unsat_reuse_counter counts the number of times a stored
282%    unsatisfiable set is re-used
283
284set_unsat_reuse_counter(Number) :- !,
285    pdl_write('set_unsat_reuse_counter to '), pdl_write(Number), pdl_nl,
286    flag(unsat_reuse_counter, _, Number).
287
288increment_unsat_reuse_counter(Increment) :- !,
289    flag(unsat_reuse_counter, Old, Old + Increment).
290
291get_unsat_reuse_counter(Number) :- !,
292    flag(unsat_reuse_counter, Number, Number).
293
294
295%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
296%
297%     The key satisfiable is used to track satisfiability on the current
298%     branch.
299%     -1 means undefined, 0 means unsatisfiable, 1 means satisfiable
300
301set_satisfiable_flag(Value) :-
302    flag(satisfiable, _, Value).
303
304get_satisfiability_status(Value) :-
305    flag(satisfiable, Value, Value).
306
307is_satisfiable(_) :-
308    get_satisfiability_status(1).
309
310is_unsatisfiable(_) :-
311    get_satisfiability_status(0).
312
313%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
314%
315% test_ignorability(+Branch,+FulfilledEventualities)
316% According to Definition 7 in (De Giacomo and Massacci, 2001),
317% a \pi-completed branch B is ignorable iff there is an eventuality X which
318% is not fulfilled. A branch is \pi-completed if (i) all prefixes are
319% reduced, i.e. all rules except <A>-rules have been applied, and
320% (ii) for every s1 which is not fully reduced there is a pair (s0,S0)
321% shorter than (s1,B) s.t. s0 is fully reduced in the segment S0 and s1 is
322% a copy of s0 in B.
323% The procedure only uses +Branch to determine all the eventualities
324% present on the branch. Whether these are fulfilled is then checked against
325% +FulfilledEventualities, a list of all eventualities currently fulfilled
326% on the branch.
327% Note that since distinct X_i and X_j can represent the
328% same eventuality, this check requires more than just comparing, say, the
329% number of syntactically distinct X_i present on the branch with the number
330% of syntactically distinct X_i in +FulfilledEventualities.
331% Note also, that we obtain +FulfilledEventualities from reduce_local.
332% +FulfilledEventualities will only be correct, as long complement splitting
333% is used to deal with X_i = <A*>F and as long rules are applied even if one
334% of the consequents is present (i.e. the formula F should not subsume <A*>F).
335
336test_ignorability(Branch, FulfilledEventualities) :-
337    eventualities(Branch, Eventualities),
338    collectCopies(Branch,Copies),
339    pdl_write_ln('In test_ignorability... '),
340    pdl_write('    Branch :    '), pdl_write(Branch), pdl_nl,
341    pdl_write('    FulfilledEventualities : '), pdl_write(FulfilledEventualities), pdl_nl,
342    pdl_write('    Eventualities :    '), pdl_write(Eventualities), pdl_nl,
343    test_ignorability_loop(Eventualities, FulfilledEventualities, Copies, Branch, _NewEventualities, _NewFulfilledEventualities).
344
345
346test_ignorability_loop(Eventualities, FulfilledEventualities, Copies, Branch, NewEventualities, NewFulfilledEventualities) :-
347	test_ignorability_aux(Eventualities, FulfilledEventualities, Copies,
348	                      NewEventualities1, NewFulfilledEventualities1),
349        (NewEventualities1 == [] ->
350	    NewEventualities = NewEventualities1,
351	    NewFulfilledEventualities = NewFulfilledEventualities1
352	;
353	    (NewFulfilledEventualities1 == FulfilledEventualities ->
354		print_unfulfilled_eventualities(NewEventualities1),
355		compute_inconsistent_sets(Eventualities,Branch,Copies),
356		!,
357		fail
358	    ;
359		test_ignorability_loop(NewEventualities1, NewFulfilledEventualities1, Copies, Branch, NewEventualities, NewFulfilledEventualities)
360	    )
361	).
362
363
364%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
365%
366% print_unfulfilled_eventualities(+Eventualities)
367%
368%   print a list of eventualities that are not fulfilled on the current branch
369
370print_unfulfilled_eventualities([]) :-
371	!.
372print_unfulfilled_eventualities([ev(State,x(Y,Fml))|Eventualities]) :-
373	pdl_write('** Ignorable ** - '), pdl_write(ev(State,x(Y,Fml))), pdl_write(' unfulfilled'), pdl_nl,
374	print_proof_step('post', '** Ignorable **', ['unfulfilled',ev(State,x(Y,Fml))]),
375%       print_proof_step('post', '** Ignorable/Unsatisfiable **', ['unfulfilled',x(Y,Fml)]),
376	!,
377	print_unfulfilled_eventualities(Eventualities).
378
379%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
380%
381% compute_inconsistent_sets(+Eventualities, +Branch, +Copies)
382%
383
384compute_inconsistent_sets([], _, _) :-
385	!.
386
387compute_inconsistent_sets([ev(State,x(_Y,_Fml))|Eventualities], Branch, Copies) :-
388	get_formulae_for_state(State,Branch,FmlList),
389	memberchk(isCopyOf(State,_),Copies),
390	store_inconsistent(FmlList),
391	!,
392	compute_inconsistent_sets(Eventualities, Branch, Copies).
393
394get_formulae_for_state(State1,[isCopyOf(_,_)|Branch],FmlList) :-
395	get_formulae_for_state(State1,Branch,FmlList),
396	!.
397get_formulae_for_state(State1,[pr(State1,FmlList)|_Branch],FmlList) :-
398	!.
399get_formulae_for_state(State1,[pr(State2,_FmlList)|Branch],FmlList) :-
400	State1 \= State2,
401	get_formulae_for_state(State1,Branch,FmlList),
402	!.
403
404%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
405%
406% test_ignorability_aux(+Eventualities, +FulfilledEventualities, +Copies,
407%                       -NewEventualities, -NewFulfilledEventualities)
408%   computes -NewEventualities and -NewFulfilledEventualities from
409%   +Eventualities and +FulfilledEventualities as follows:
410%   -NewFulfilledEventualities contains all eventualities in +FulfilledEventualities
411%   plus any eventuality in +Eventualities that can be shown to be fulfilled with
412%   respect to +FulfilledEventualities and +Copies;
413%   -NewEventualities contains all eventualities in +Eventualities that cannot be
414%   shown to be fulfilled with respect to +FulfilledEventualties and +Copies.
415
416test_ignorability_aux([], FulfilledEventualities, _Copies, [], FulfilledEventualities).
417
418test_ignorability_aux([ev(State,Eventuality)|Eventualities], FulfilledEventualities, Copies, NewEventualities, NewFulfilledEventualities) :-
419    (test_ignorability_aux_fml(ev(State,Eventuality), FulfilledEventualities, Copies) ->
420	append(FulfilledEventualities,[fulfilled(State,Eventuality)],NewFulfilledEventualities1),
421	test_ignorability_aux(Eventualities, NewFulfilledEventualities1, Copies, NewEventualities, NewFulfilledEventualities)
422    ;
423	test_ignorability_aux(Eventualities, FulfilledEventualities, Copies, NewEventualities1, NewFulfilledEventualities),
424	NewEventualities = [ev(State,Eventuality)|NewEventualities1]
425    ).
426
427%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
428%
429% test_ignorability_aux_fml(+Eventuality, +FulfilledEventualities, +Copies)
430%
431% succeeds if +Eventuality is a fulfilled eventuality. This in turn is the case
432% if (a) among +FulfilledEventualities is a syntactically identical eventuality
433% which is already recorded as being fulfilled on the current branch, or
434% (b) among +FulfilledEventualities is an eventuality Eventuality2, recorded to
435% be fulfilled at a state State2 such that the state State1 at which +Eventuality
436% occurs collapsed to State2.
437
438test_ignorability_aux_fml(_, [], _) :-
439	fail.
440
441test_ignorability_aux_fml(ev(State1,x(Y,Fml)), [fulfilled(State2, x(X,Fml))|_], Copies) :-
442	(X = Y ->
443	    print_proof_step('post', fulfilled_by(ev(State1,x(Y,Fml)), ev(State2,x(X,Fml))), '[fulfilled]')
444	;
445	    collapses(State1,State2,Copies),
446	    print_proof_step('post', fulfilled_by(ev(State1,x(Y,Fml)), ev(State2,x(X,Fml))), '[fulfilled]')
447	).
448
449test_ignorability_aux_fml(Event, [_|FulfilledEventualities], Copies) :-
450    test_ignorability_aux_fml(Event, FulfilledEventualities, Copies).
451
452
453%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
454%
455% collectCopies(+Branch, -Copies)
456%
457% whenever a state State1 is identified as a copy of a State2, we record that
458% fact by adding isCopyOf(State1,State2)' on a branch. The predice collectCopies
459% retrieves all such facts from +Branch and returns it as a list -Copies.
460
461collectCopies([isCopyOf(State1,State2)|Branch],[isCopyOf(State1,State2)|Copies]) :-
462	!,
463	collectCopies(Branch,Copies).
464collectCopies([_|Branch],Copies) :-
465	collectCopies(Branch,Copies),
466	!.
467collectCopies([],[]).
468
469%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
470%
471% collapses(+State1, +State2, +Copies)
472%
473% succeeds if +State1 is a copy of +State2 with respect to the information on
474% which states are copies of each other contained in +Copies.
475
476collapses(X, Y, Copies) :-
477	memberchk(isCopyOf(X,Y),Copies).
478
479
480%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
481%
482% test_unsatisfiability(+State, +FmlList, +CompleteFmlList)
483%
484%   test for inconsistency of the list of formulae FmlList;
485%   - The first rule states that the empty set/list of formulae is not
486%     inconsistent
487%   - The second rule covers conditions 1 and 2 of Definition 23 in %
488%     (De Giacomo and Massacci, 2000) via a inf_closure
489%   - The third rule  covers condition 3 of Definition 23 in
490%     (De Giacomo and Massacci, 2000)
491
492test_unsatisfiability(_, [], _) :- !.
493% The following rule uses condition 3 of Definition 23 in
494% (De Giacomo and Massacci, 2000):
495% A superset of a \bot-set is a \bot-set.
496test_unsatisfiability(State, Fml, _) :-
497    list_to_ord_set(Fml,OrdFml1),
498    inconsistent(OrdFml2),
499    ord_subset(OrdFml2,OrdFml1),
500    pdl_write('Reused unsatisfiable set '), pdl_write(OrdFml2), pdl_nl,
501    print_proof_step(State, inconsistent_subset_of(OrdFml2,OrdFml1), '[inconsistent subset]'),
502    increment_unsat_reuse_counter(1),
503    !,
504    fail.
505test_unsatisfiability(State, Set, CompleteFmlList) :-
506    select_fml(Given, Set, SetWithoutGiven),
507    inf_closure(State, Given, SetWithoutGiven, CompleteFmlList),
508    test_unsatisfiability(State, SetWithoutGiven, CompleteFmlList).
509
510%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
511
512select_fml(Fml, [Fml|FmlList], FmlList).
513
514%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
515%
516% is_copy(+FmlList, +CurrentState, +Branch).
517%
518%     test if pr(CurrentState, FmlList) is a copy of an earlier state in
519%     Branch.
520
521is_copy(_,_,[],_) :-
522	fail.
523is_copy(FmlList, State, [isCopyOf(_,_)|Branch], EqualStates) :-
524	!,
525	is_copy(FmlList, State, Branch, EqualStates).
526is_copy(FmlList, State, [pr(X,FmlListInX)|_],isCopyOf(State,X)) :-
527	is_prefix(X, State),
528	% Ignore the first argument in the introduce literals x(_,Fml)
529        simplify_X(FmlList, SimplifiedFmlList),
530	simplify_X(FmlListInX, SimplifiedFmlListInX),
531%    pdl_write_ln('In is_copy... '),
532%    pdl_write('    SimplifiedFmlList :    '), pdl_write(SimplifiedFmlList), pdl_nl,
533%    pdl_write('    SimplifiedFmlListInX : '), pdl_write(SimplifiedFmlListInX), pdl_nl,
534    equal_set(SimplifiedFmlList, State, SimplifiedFmlListInX, X), !.
535is_copy(FmlList, State, [pr(_,_)|Branch], EqualStates) :-
536	is_copy(FmlList, State, Branch, EqualStates).
537
538%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
539
540is_prefix(X, X).
541is_prefix(X, ((Y), _)) :-
542    is_prefix(X,Y).
543
544prefix_to_list(0,[0]) :- !.
545prefix_to_list(((X), L, N),List) :-
546	prefix_to_list(X,List1),
547	append(List1,[L,N],List),
548	!.
549
550list_to_prefix([0],(0)) :- !.
551list_to_prefix([A,B|List],(Prefix1,L,N)) :-
552	append(PrefixList,[L,N],[A,B|List]),
553	list_to_prefix(PrefixList,Prefix1),
554	!.
555
556%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
557
558equal_set([], State, [], X) :- !,
559    % X is a copy of State
560    print_copies(State, X).
561
562equal_set([Elem|Set1], State, Set2, X) :-
563    delete(Set2, Elem, Set3),
564    equal_set(Set1, State, Set3, X).
565
566%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
567
568eliminate_duplicates(List, SimplifiedList) :- !,
569    sort(List, SimplifiedList).
570
571%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
572%
573% complement(+Fml,-NotFml)
574%
575%     Returns the complement of Fml.
576
577complement(not(A),A) :- !.
578
579complement(A,not(A)) :- !.
580
581%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
582%
583% reduce_existentials(+Axioms, +Existential, +State,
584%        +Universal, +Branch, -NewBranch,
585%        +Eventualities, -NewEventualities)
586%
587%     - Applies existential, universal and theory rules
588%
589
590reduce_existentials(_, [], _, _, Branch, Branch,
591              Eventualities, Eventualities, IDT, IDT).
592
593reduce_existentials(Axioms, Existential, X, Universal, Branch, NewBranch,
594              Eventualities, NewEventualities, IDT, ODT) :-  !,
595%    pdl_write('In reduce_existentials, X : '), pdl_write(X), pdl_nl,
596%    pdl_write('    Existential : '), pdl_write(Existential), pdl_nl,
597    select(Fml, Existential, ExistentialWithoutFml),
598    Fml = dia(R,A),
599    pdl_write('* R = '), pdl_write(R),
600%    atom(R),
601    pdl_write_ln('* '),
602    increment_states_counter(1),
603    get_states_counter(N),
604    Y = (X,R,N),
605    print_proof_step(Y, A, ['dia',Fml]),
606%    pdl_write('In reduce_existentials, Y : '), pdl_write(Y), pdl_nl,
607
608    reduce_universal(Universal, Y, [], Unexpanded),
609
610    extend_unexpanded([A], [], Unexpanded, NewUnexpanded),
611    reduce_existential(Axioms, NewUnexpanded, Y, Branch, NewBranch1,
612                  Eventualities, NewEventualities1, IDT, ODT_RE),
613    reduce_existentials(Axioms, ExistentialWithoutFml, X, Universal,
614                  NewBranch1, NewBranch, NewEventualities1, NewEventualities, ODT_RE, ODT).
615
616
617reduce_existential(Axioms, NewUnexpanded, Y, Branch, NewBranch,
618                   Eventualities, NewEventualities, IDT, ODT) :-
619    search_state(Axioms, NewUnexpanded, Y, Branch, NewBranch,
620                 Eventualities, NewEventualities, IDT, ODT).
621
622
623%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
624
625reduce_universal([], _, Unexpanded, Unexpanded).
626
627reduce_universal([not(dia(R,A))|Universal], Y, Unexpanded, NewUnexpanded) :-
628    % check if Y is an R-successor
629    Y = (_,R,_), !,
630    complement(A, NotA),
631    extend_unexpanded([NotA], [], Unexpanded, NewUnexpanded1,
632                 Y, ['box',not(dia(R,A))]),
633    reduce_universal(Universal, Y, NewUnexpanded1, NewUnexpanded).
634
635reduce_universal([_|Universal], Y, Unexpanded, NewUnexpanded) :-
636    reduce_universal(Universal, Y, Unexpanded, NewUnexpanded).
637
638%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
639%
640% extend_unexpanded(+FmlList, +Workedoff, +Unexpanded, -NewUnexpanded,
641%                   +X, +Justification)
642% - Adds all non-redundant formulae in FmlList to Unexpanded;
643%   redundancy is evaluated against Workedoff
644% - Keeping all expanded formulae in Workedoff has the disadvantage that
645%   the performance decreases and proofs are longer.
646%
647% TO DO: Consider ways of reducing this bookkeeping while preserving
648% soundness and completeness.
649%
650
651extend_unexpanded([], _, Unexpanded, Unexpanded, _, _).
652
653extend_unexpanded([Fml|Rest], Workedoff, Unexpanded, NewUnexpanded, X, Justification) :-
654    extend_unexpanded_aux(Fml, Workedoff, Unexpanded, Unexpanded1,
655                     X, Justification), !,
656    extend_unexpanded(Rest, Workedoff, Unexpanded1, NewUnexpanded, X, Justification).
657
658extend_unexpanded_aux(true, _, Unexpanded, Unexpanded,
659                 X, Justification) :-
660    print_proof_step(X, '-', Justification).
661
662extend_unexpanded_aux(Fml, Workedoff, Unexpanded, [Fml|Unexpanded],
663                 X, Justification) :-
664    not_redundant(Fml, Workedoff, Unexpanded),
665    print_proof_step(X, Fml, Justification).
666
667extend_unexpanded_aux(Fml, _, Unexpanded, Unexpanded, X, Justification) :-
668    print_redundant_step(X, Fml, Justification).
669
670%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
671%
672% extend_unexpanded(+FmlList, +Workedoff, +Unexpanded, -NewUnexpanded)
673%
674%     Same as above, but derivation step is not documented
675%
676
677extend_unexpanded([], _, Unexpanded, Unexpanded).
678
679extend_unexpanded([Fml|Rest], Workedoff, Unexpanded, NewUnexpanded) :-
680    extend_unexpanded_aux(Fml, Workedoff, Unexpanded, Unexpanded1), !,
681    extend_unexpanded(Rest, Workedoff, Unexpanded1, NewUnexpanded).
682
683extend_unexpanded_aux(Fml, Workedoff, Unexpanded, [Fml|Unexpanded]) :-
684    not_in_set(Fml, Workedoff),
685    not_in_set(Fml, Unexpanded).
686
687extend_unexpanded_aux(_, _, Unexpanded, Unexpanded) :-
688    true.
689
690%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
691% not_in_set(+Fml, +FmlList)
692%
693
694not_redundant(Fml, FmlList1, FmlList2) :-
695    not_in_set(Fml, FmlList1),
696    not_in_set(Fml, FmlList2).
697
698%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
699% not_in_set(+Fml, +FmlList)
700%
701
702not_in_set(Fml, FmlList) :-
703    \+ member(Fml, FmlList).
704
705%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
706% known_consistent(Fmls)
707% If Fmls is a subset of a set of formulae which is already known to be
708% consistent, then Fmls is also consistent
709%
710
711known_consistent(Fmls,BranchForFmls,EventualitiesForFmls) :-
712	list_to_ord_set(Fmls,OrdFmls1),
713	consistent(OrdFmls2,BranchForFmls,EventualitiesForFmls),
714	ord_subset(OrdFmls1,OrdFmls2),
715%	write('Reused satisfiable set '), print(OrdFmls2), nl,
716%	write('Reused a satisfiable set '), nl,
717	print_proof_step(g, consistent_superset_of(OrdFmls2,OrdFmls1), '[consistent superset]'),
718	increment_sat_reuse_counter(1),
719	!.
720
721%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
722% print_copies(+State, +CopyState)
723%
724
725print_copies(State, CopyState) :-
726    print_proof_step(State, copy_of(State, CopyState), '[loop checking]').
727
728%%print_copies(State, CopyState) :-
729%%    sprintf_state(StateString, State),
730%%    string_to_atom(StateString, State1),
731%%    sprintf_state(CopyStateString, CopyState),
732%%    swritef(String, 'copy of %w', [CopyStateString]),
733%%    string_to_atom(String, StringAtom),
734%%    print_proof_step(State1, StringAtom, 'loop checking').
735
736%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
737
738print_result(Result) :-
739    write('** '), write(Result), write_ln(' **'),
740    get_search_output_filename(Filename),
741    append(Filename),
742    (get_output_format(latex) ->
743	write('& \\text{** '), write(Result), write_ln(' **}')
744    ;
745	write('** '), write(Result), write_ln(' **')
746    ),
747    told.
748
749%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
750
751print_proof_step(_, [], _) :- !.
752
753print_proof_step(State, [Fml|FmlList], Justification) :- !,
754    print_proof_step(State, Fml, Justification),
755    print_proof_step(State, FmlList, Justification).
756
757print_proof_step(State, Conclusion, Justification) :-
758    increment_proof_steps_counter(1),
759    get_proof_steps_counter(N),
760%    print_proof_step_aux(N, State, Conclusion, Justification),
761    get_search_output_filename(Filename),
762    append(Filename),
763    (get_output_format(latex) ->
764         print_proof_step_latex(N, State, Conclusion, Justification)
765    ;
766	print_proof_step_aux(N, State, Conclusion, Justification)
767    ),
768    told.
769
770print_proof_step_aux(N, State, Conclusion, Justification) :-
771    pdl_writef('%4r.  ', [N]),
772    get_branch_point_counter(Count),
773    pdl_tab(Count * 4),
774    print_state(State), pdl_write(' : '),
775    print_conclusion(Conclusion), pdl_nl,
776    pdl_write('    '),
777%    pdl_write('                        '),
778    pdl_write(Justification), pdl_nl.
779
780
781print_proof_step_latex(N, State, Conclusion, Justification) :-
782    pdl_write(N), pdl_write('.\\  & '),
783    get_branch_point_counter(Count),
785    print_state_latex(State), pdl_write(' {:} '),
786    print_conclusion_latex(Conclusion), pdl_nl,
787    pdl_write('\\tag*{$'), 788 print_justification_latex(Justification), !, 789 pdl_write('$}'), pdl_nl,
790    pdl_write('\\\\'), pdl_nl.
791
793
796    CountDecr is Count - 1,
798
799
800%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
801
802print_redundant_step(_, [], _) :- !.
803
804print_redundant_step(State, [Fml|FmlList], Justification) :- !,
805    print_redundant_step(State, Fml, Justification),
806    print_redundant_step(State, FmlList, Justification).
807
808print_redundant_step(State, Conclusion, Justification) :-
809    print_proof_step_aux('-', State, Conclusion, Justification),
810    get_search_output_filename(Filename),
811    append(Filename),
812    (get_output_format(latex) ->
813         print_proof_step_latex('-', State, Conclusion, Justification)
814    ;
815	print_proof_step_aux('-', State, Conclusion, Justification)
816    ),
817    told.
818
819%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
820
821print_justification_latex(String) :-
822    atom(String), !,
823    rule_name_latex(String, LatexString),
824    pdl_write(LatexString).
825
826print_justification_latex([String|FmlList]) :-
827    atom(String), !,
828    rule_name_latex(String, LatexString),
829    pdl_write(LatexString), pdl_write('{}: '),
830    print_formula_list_latex(FmlList).
831
832print_justification_latex(Justification) :- !,
833    pdl_write(Justification).
834
835%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
836
837rule_name_latex(true, '\\mltop').
838rule_name_latex('or-LEFT', '\\text{${\\mlor}$-left}').
839rule_name_latex('or-RIGHT', '\\text{${\\mlor}$-right}').
840rule_name_latex('or-RIGHT1', '\\text{${\\mlor}$-right1}').
841rule_name_latex('or-RIGHT2', '\\text{${\\mlor}$-right2}').
842rule_name_latex('and', '\\neg{\\mlor}').
843%rule_name_latex('and', '{\\mland}').
844rule_name_latex('dia-or-LEFT', '\\text{$\\mldia{\\mlor}{}$-left}').
845rule_name_latex('dia-or-RIGHT', '\\text{$\\mldia{\\mlor}{}$-right}').
846rule_name_latex('dia-or-RIGHT1', '\\text{$\\mldia{\\mlor}{}$-right1}').
847rule_name_latex('dia-or-RIGHT2', '\\text{$\\mldia{\\mlor}{}$-right2}').
848rule_name_latex('dia-comp', '\\mldia{\\comp{}{}}{}').
849rule_name_latex('dia-star', '\\mldia{\\ast}{}').
850rule_name_latex('dia-test', '\\mldia{?}{}').
851rule_name_latex('dia', '\\mldia{\\cdot}{}').
852rule_name_latex('X-LEFT', '\\text{$X$-left}').
853rule_name_latex('X-RIGHT', '\\text{$X$-right}').
854rule_name_latex('X-RIGHT1', '\\text{$X$-right1}').
855rule_name_latex('X-RIGHT2', '\\text{$X$-right2}').
856rule_name_latex('box-or', '\\neg\\mldia{\\mlor}{}').
857rule_name_latex('box-comp', '\\neg\\mldia{\\comp{}{}}{}').
858rule_name_latex('box-star', '\\neg\\mldia{\\ast}{}').
859rule_name_latex('box-test-LEFT', '\\text{$\\neg\\mldia{?}{}$-left}').
860rule_name_latex('box-test-RIGHT', '\\text{$\\neg\\mldia{?}{}$-right}').
861rule_name_latex('box-test-RIGHT1', '\\text{$\\neg\\mldia{?}{}$-right1}').
862rule_name_latex('box-test-RIGHT2', '\\text{$\\neg\\mldia{?}{}$-right2}').
863rule_name_latex('box', '\\neg\\mldia{\\cdot}{}').
864%rule_name_latex('box-or', '\\mlbox{\\mlor}{}').
865%rule_name_latex('box-comp', '\\mlbox{\\comp}{}').
866%rule_name_latex('box-star', '\\mlbox{\\ast}{}').
867%rule_name_latex('box', '\\mlbox{\\cdot}{}').
868rule_name_latex('[theory]', '\\text{theory}').
869rule_name_latex('[theory-inst]', '\\text{theory-inst}').
870rule_name_latex('[given]', '\\text{given}').
871rule_name_latex('[fulfilled]', '\\text{fulfilled}').
872rule_name_latex('[loop checking]', '\\text{loop checking}').
873rule_name_latex(String, LatexString) :-
874    swritef(LatexString, '\\\\text{%w}', [String]).
875
876%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
877
878justification_latex('[given]', 'given').
879justification_latex('[fulfilled]', 'fulfilled').
880justification_latex('[loop checking]', 'loop checking').
881
882%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
883
884print_formula_list_latex([]).
885
886print_formula_list_latex([Fml]) :-
887    print_formula_latex(Fml).
888
889print_formula_list_latex([Fml|List]) :-
890    print_formula_latex(Fml),
891    pdl_write(', '),
892    print_formula_list_latex(List).
893
894%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
895
896print_formula_latex(true) :- !,
897    pdl_write('\\mltop').
898
899print_formula_latex(false) :- !,
900    pdl_write('\\mlbot').
901
902print_formula_latex(x(Y,Fml)) :- !,
903    pdl_write('X^{'), print_state(Y), pdl_write('}_{'),
904    print_formula_latex(Fml), pdl_write('}').
905
906print_formula_latex(ev(State,x(Y,Fml))) :- !,
907    print_state(State), pdl_write(' {:} '),
908    pdl_write('X^{'), print_state(Y), pdl_write('}_{'),
909    print_formula_latex(Fml), pdl_write('}').
910print_formula_latex(at(State,Fml)) :- !,
911    print_state(State), pdl_write(' {:} '),
912    print_formula_latex(Fml).
913
914print_formula_latex(and(A,B)) :- !,
915    pdl_write('('),
916    print_formula_latex(A),
917    pdl_write(' \\mland '),
918    print_formula_latex(B),
919    pdl_write(')').
920
921print_formula_latex(or(A,B)) :- !,
922    pdl_write('('),
923    print_formula_latex(A),
924    pdl_write(' \\mlor '),
925    print_formula_latex(B),
926    pdl_write(')').
927
928print_formula_latex(not(A)) :- !,
929    pdl_write('\\neg '),
930    print_formula_latex(A).
931
932print_formula_latex(test(A)) :- !,
933    pdl_write('\\test{'),
934    print_formula_latex(A),
935    pdl_write('}').
936
937print_formula_latex(comp(A,B)) :- !,
938    pdl_write('(\\comp{'),
939    print_formula_latex(A),
940    pdl_write('}{'),
941    print_formula_latex(B),
942    pdl_write('})').
943
944print_formula_latex(star(A)) :- !,
945    print_formula_latex(A),
946    pdl_write('{}^*').
947
948print_formula_latex(dia(R,A)) :- !,
949    pdl_write('\\mldia{'),
950    print_formula_latex(R),
951    pdl_write('}{'),
952    print_formula_latex(A),
953    pdl_write('}').
954
955print_formula_latex(box(R,A)) :- !,
956    pdl_write('\\mlbox{'),
957    print_formula_latex(R),
958    pdl_write('}{'),
959    print_formula_latex(A),
960    pdl_write('}').
961
962print_formula_latex(A) :- !,
963    pdl_write('\\textit{'), pdl_write(A), pdl_write('}').
964
965%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
966
967latex_output(begin) :- !,
968    get_search_output_filename(Filename),
969    append(Filename),
970    pdl_write_ln('\\begin{align*}'),
971    told.
972
973latex_output(end) :- !,
974    get_search_output_filename(Filename),
975    append(Filename),
976    pdl_write_ln('\\end{align*}'),
977    told.
978
979%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
980
981sprintf_state(String, (X,Y)) :- !,
982    sprintf_state(XString, X),
983    sprintf_state(YString, Y),
984    swritef(String, '%w.%w', [XString, YString]).
985
986sprintf_state(XString,X) :-
987    string_to_atom(XString, X).
988
989%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
990
991print_state((X,Y)) :- !,
992    print_state(X), pdl_write('.'), print_state(Y).
993
994print_state(X) :-
995    pdl_write(X).
996
997%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
998
999print_state_latex((X,Y)) :- !,
1000    print_state_latex(X), pdl_write('.'), print_state_latex(Y).
1001
1002print_state_latex(X) :-
1003    number(X), !,
1004    pdl_write(X).
1005
1006print_state_latex(X) :- !,
1007    pdl_write('\\textit{'), pdl_write(X), pdl_write('}').
1008
1009%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1010
1011print_conclusion(fulfilled_by(Fml1,Fml2)) :- !,
1012    pdl_write('\\ '), pdl_write(Fml1), pdl_write(' fulfilled by '), pdl_write(Fml2).
1013
1014print_conclusion(copy_of(X,Y)) :- !,
1015    print_state(X), pdl_write(' copy of '), print_state(Y).
1016
1017print_conclusion(inconsistent_subset_of(X,Y)) :- !,
1018    print_state(X), pdl_write(' is an inconsistent subset of '), print_state(Y).
1019
1020print_conclusion(consistent_superset_of(X,Y)) :- !,
1021    print_state(X), pdl_write(' is a consistent superset of '), print_state(Y).
1022
1023print_conclusion(inconsistent_set(X)) :- !,
1024    print_state(X), pdl_write(' is an inconsistent set').
1025
1026print_conclusion(consistent_set(X)) :- !,
1027    print_state(X), pdl_write(' is an consistent set').
1028
1029print_conclusion(X) :-
1030    pdl_write(X).
1031
1032%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1033
1034print_conclusion_latex(fulfilled_by(Fml1,Fml2)) :- !,
1035    pdl_write(' '),
1036    print_formula_latex(Fml1),
1037    pdl_write('\\textit{ fulfilled by }'),
1038    print_formula_latex(Fml2).
1039
1040print_conclusion_latex(copy_of(X,Y)) :- !,
1041    print_state_latex(X),
1042    pdl_write('\\textit{ copy of }'),
1043    print_state_latex(Y).
1044
1045print_conclusion_latex(consistent_set(X)) :- !,
1046    pdl_write('\\begin{array}[t]{l}'), pdl_nl,
1047    print_formula_list_latex(X), pdl_write('\\\\ '), pdl_nl,
1048    pdl_write('\\textit{ is a consistent set }'), pdl_nl,
1049    pdl_write('\\end{array}').
1050
1051print_conclusion_latex(inconsistent_set(X)) :- !,
1052    pdl_write('\\begin{array}[t]{l}'), pdl_nl,
1053    print_formula_list_latex(X), pdl_write('\\\\ '), pdl_nl,
1054    pdl_write('\\textit{ is an inconsistent set }'), pdl_nl,
1055    pdl_write('\\end{array}').
1056
1057print_conclusion_latex(consistent_superset_of(X,Y)) :- !,
1058    pdl_write('\\begin{array}[t]{l}'), pdl_nl,
1059    print_formula_list_latex(X), pdl_write('\\\\ '), pdl_nl,
1060    pdl_write('\\textit{ is a consistent superset of }\\\\ '), pdl_nl,
1061    print_formula_list_latex(Y), pdl_write('\\\\ '), pdl_nl,
1062    pdl_write(' \\end{array}').
1063
1064print_conclusion_latex(inconsistent_subset_of(X,Y)) :- !,
1065    pdl_write('\\begin{array}[t]{l}'), pdl_nl,
1066    print_formula_list_latex(X), pdl_write('\\\\ '), pdl_nl,
1067    pdl_write('\\textit{ is an inconsistent subset of }\\\\ '), pdl_nl,
1068    print_formula_list_latex(Y), pdl_write('\\\\ '), pdl_nl,
1069    pdl_write(' \\end{array}').
1070
1071print_conclusion_latex(X) :-
1072    print_formula_latex(X).
1073
1074%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1075
1076print_list([]).
1077
1081    print_list(List)`