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),
  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
  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
 1078print_list([Head|List]) :-
 1079    pdl_write(Head), 
 1080    pdl_write(' '),
 1081    print_list(List)