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 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 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 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
55
56satisfiable(Fml, Result) :-
57 satisfiable([], Fml, Result).
58
59satisfiable(Axioms, FmlInput, satisfiable) :-
60 retractall(consistent(_,_,_)),
61 retractall(inconsistent(_)),
62 63 create_search_output_file,
64
65 FmlInput = Fml,
66
67 nl,
68 pdl_write('** Input: '), pdl_write(Fml), pdl_nl,
69
70 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 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
99
100negated_formula(Fml, not(Fml)) :-
101 get_negate_first(yes), !.
102
103negated_formula(Fml, Fml).
104
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),
133 print_result('Satisfiable branch found').
134
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 157 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
197
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) :-
212 reduce_existentials(Axioms, SimplifiedExistential, State,
213 SimplifiedUniversal, ExtendedBranch, NewBranch,
214 ExtendedEventualities, NewEventualities, IDT, ODT).
215
219
220extend_branch(State, FmlList, Branch, [pr(State, FmlList)|Branch]).
221
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
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
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
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
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
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
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
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))]),
376 !,
377 print_unfulfilled_eventualities(Eventualities).
378
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
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
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
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
475
476collapses(X, Y, Copies) :-
477 memberchk(isCopyOf(X,Y),Copies).
478
479
491
492test_unsatisfiability(_, [], _) :- !.
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
511
512select_fml(Fml, [Fml|FmlList], FmlList).
513
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 529 simplify_X(FmlList, SimplifiedFmlList),
530 simplify_X(FmlListInX, SimplifiedFmlListInX),
534 equal_set(SimplifiedFmlList, State, SimplifiedFmlListInX, X), !.
535is_copy(FmlList, State, [pr(_,_)|Branch], EqualStates) :-
536 is_copy(FmlList, State, Branch, EqualStates).
537
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
557
558equal_set([], State, [], X) :- !,
559 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
567
568eliminate_duplicates(List, SimplifiedList) :- !,
569 sort(List, SimplifiedList).
570
576
577complement(not(A),A) :- !.
578
579complement(A,not(A)) :- !.
580
589
590reduce_existentials(_, [], _, _, Branch, Branch,
591 Eventualities, Eventualities, IDT, IDT).
592
593reduce_existentials(Axioms, Existential, X, Universal, Branch, NewBranch,
594 Eventualities, NewEventualities, IDT, ODT) :- !,
597 select(Fml, Existential, ExistentialWithoutFml),
598 Fml = dia(R,A),
599 pdl_write('* R = '), pdl_write(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]),
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
624
625reduce_universal([], _, Unexpanded, Unexpanded).
626
627reduce_universal([not(dia(R,A))|Universal], Y, Unexpanded, NewUnexpanded) :-
628 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
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
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
693
694not_redundant(Fml, FmlList1, FmlList2) :-
695 not_in_set(Fml, FmlList1),
696 not_in_set(Fml, FmlList2).
697
701
702not_in_set(Fml, FmlList) :-
703 \+ member(Fml, FmlList).
704
710
711known_consistent(Fmls,BranchForFmls,EventualitiesForFmls) :-
712 list_to_ord_set(Fmls,OrdFmls1),
713 consistent(OrdFmls2,BranchForFmls,EventualitiesForFmls),
714 ord_subset(OrdFmls1,OrdFmls2),
717 print_proof_step(g, consistent_superset_of(OrdFmls2,OrdFmls1), '[consistent superset]'),
718 increment_sat_reuse_counter(1),
719 !.
720
724
725print_copies(State, CopyState) :-
726 print_proof_step(State, copy_of(State, CopyState), '[loop checking]').
727
735
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
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),
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(' '),
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),
784 print_quad(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
792print_quad(0).
793
794print_quad(Count) :-
795 pdl_write('\\quad\\qquad '),
796 CountDecr is Count - 1,
797 print_quad(CountDecr).
798
799
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
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
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}').
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}{}').
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
877
878justification_latex('[given]', 'given').
879justification_latex('[fulfilled]', 'fulfilled').
880justification_latex('[loop checking]', 'loop checking').
881
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
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
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
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
990
991print_state((X,Y)) :- !,
992 print_state(X), pdl_write('.'), print_state(Y).
993
994print_state(X) :-
995 pdl_write(X).
996
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
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
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
1075
1076print_list([]).
1077
1078print_list([Head|List]) :-
1079 pdl_write(Head),
1080 pdl_write(' '),
1081 print_list(List)