%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Copyright 2003-2010, Renate Schmidt, University of Manchester
% 2009-2010, Ullrich Hustadt, University of Liverpool
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
prove(Fml, Result) :-
provable([], Fml, Result).
provable(Fml, Result) :-
provable([], Fml, Result).
provable(Axioms, FmlInput, unprovable) :-
retractall(consistent(_,_,_)),
retractall(inconsistent(_)),
retractall(reduced(_,_,_)),
% Axioms is a set of non-logical axioms, i.e. a background theory
create_search_output_file,
negated_formula(FmlInput, Fml),
nl,
pdl_write('** Input: '), pdl_write(Fml), pdl_nl,
% Transform Axioms and Fml into negation normal form
pdl_write('** NFAxioms: '), pdl_nl,
normalise(Axioms, NFAxioms),
normalise(Fml, [], NFFml, Paths),
pdl_write('** NFFml: '), pdl_write(NFFml), pdl_nl,
pdl_write('Paths = '), pdl_write(Paths), pdl_nl,
(get_output_format(latex) ->
latex_output(begin)
;
true),
% Search for a proof or a model
search(NFAxioms, NFFml), !,
(get_output_format(latex) ->
latex_output(end)
;
true).
provable(_, _, provable) :-
print_result('Refutation proof found'),
(get_output_format(latex) ->
latex_output(end)
;
true).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
satisfiable(Fml, Result) :-
satisfiable([], Fml, Result).
satisfiable(Axioms, FmlInput, satisfiable) :-
retractall(consistent(_,_,_)),
retractall(inconsistent(_)),
% Axioms is a set of non-logical axioms, i.e. a background theory
create_search_output_file,
FmlInput = Fml,
nl,
pdl_write('** Input: '), pdl_write(Fml), pdl_nl,
% Transform Axioms and Fml into negation normal form
pdl_write('** NFAxioms: '), pdl_nl,
normalise(Axioms, NFAxioms),
normalise(Fml, [], NFFml, Paths),
pdl_write('** NFFml: '), pdl_write(NFFml), pdl_nl,
pdl_write('Paths = '), pdl_write(Paths), pdl_nl,
(get_output_format(latex) ->
latex_output(begin)
;
true),
% Search for a proof or a model
search(NFAxioms, NFFml), !,
(get_output_format(latex) ->
latex_output(end)
;
true).
satisfiable(_, _, unsatisfiable) :-
print_result('Refutation found'),
(get_output_format(latex) ->
latex_output(end)
;
true).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
negated_formula(Fml, not(Fml)) :-
get_negate_first(yes), !.
negated_formula(Fml, Fml).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% search(+Axioms, +Formula)
%
% Formula is a term including the formula to be tested for
% satisfiability and encodings of the positions of all subformulae
% The formula is in negation normal form.
search(Axioms, Fml) :-
set_satisfiable_flag(-1),
set_states_counter(0),
set_proof_steps_counter(-1),
set_branch_point_counter(0),
set_sat_reuse_counter(0),
set_unsat_reuse_counter(0),
print_proof_step(0, Axioms, '[theory]'),
print_proof_step(0, Fml, '[given]'),
search_state(Axioms, [Fml], 0, [], NewBranch, [], NewEventualities, [], _),
pdl_write('In search, State : '), pdl_write(0), pdl_nl,
pdl_write(' Axioms : '), pdl_write(Axioms), pdl_nl,
pdl_write(' NewBranch : '), pdl_write(NewBranch), pdl_nl,
pdl_write(' NewEventualities : '), pdl_write(NewEventualities), pdl_nl,
test_ignorability(NewBranch, NewEventualities),
% write('Remembering consistent set - state shown consistent'), write(FmlList), nl,
% print_proof_step(State, consistent_set(FmlList), '[consistent set]'),
% store_consistent(FmlList,Branch,NewBranch,Eventualities,NewEventualities)
print_result('Satisfiable branch found').
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% search_state(+Axioms, +Unexpanded, +State, +Branch, -NewBranch,
% +Eventualities, -NewEventualities)
%
% Test whether a model for < State : Unexpanded > can be constructed.
% The formulae in Unexpanded are assumed to be in negation normal form.
% * +Branch is the branch constructed so far (i.e. the segment from the
% root state/world to the parent state/world of +State)
% * -NewBranch will be a \pi-completed branch extending +Branch
% * +Eventualities will be the eventualities fulfilled so far on +Branch
% * -NewEventualities will be eventualities fulfilled on -NewBranch
% Note: The predicate search_state is also used in reduce_existentials.
search_state(Axioms, Unexpanded, State, Branch, NewBranch,
Eventualities, NewEventualities, IDT, ODT) :-
pdl_write('In search_state, State : '), pdl_write(State), pdl_nl,
pdl_write(' Unexpanded : '), pdl_write(Branch), pdl_nl,
print_proof_step(State, Axioms, '[theory-inst]'),
append(Unexpanded, Axioms, UnexpandedPlusAxioms),
% Remember: +LocalEventualities in the following call to reduce_local are
% the eventualities fulfilled in the current state +State
reduce_local(UnexpandedPlusAxioms, State, [], Workedoff,
Universal, Existential, LocalEventualities, IDT, ODT_RL),
eliminate_duplicates(Workedoff, SimplifiedWorkedoff),
eliminate_duplicates(Universal, SimplifiedUniversal),
eliminate_duplicates(Existential, SimplifiedExistential),
pdl_write(' Branch : '), pdl_write(Branch), pdl_nl,
pdl_write(' SimplifiedWorkedoff : '), pdl_write(SimplifiedWorkedoff), pdl_nl,
pdl_write(' SimplifiedUniversal : '), pdl_write(SimplifiedUniversal), pdl_nl,
pdl_write(' SimplifiedExistential : '), pdl_write(SimplifiedExistential), pdl_nl,
pdl_write(' LocalEventualities : '), pdl_write(LocalEventualities), pdl_nl,
test_unsatisfiability(State, SimplifiedWorkedoff, SimplifiedWorkedoff),
merge_set(SimplifiedWorkedoff, SimplifiedExistential, Aux),
merge_set(Aux, SimplifiedUniversal, FmlList),
pdl_write(' FmlList : '), pdl_write(FmlList), pdl_nl,
prefix_to_list(State,StateList),
assert(reduced(ODT_RL, StateList, FmlList)),
(known_consistent(FmlList,BranchForFmlList,EventualitiesForFmlList) ->
pdl_write(' is known to be consistent'), pdl_nl,
append(BranchForFmlList,Branch,NewBranch),
append(EventualitiesForFmlList,Eventualities,NewEventualities)
;
extend_branch(State, FmlList, Branch, ExtendedBranch),
pdl_write(' ExtendedBranch : '), pdl_write(ExtendedBranch), pdl_nl,
merge_set(Eventualities, LocalEventualities, ExtendedEventualities),
pdl_write(' ExtendedEventualities : '), pdl_write(ExtendedEventualities), pdl_nl,
search_state_aux(Axioms, SimplifiedExistential,
SimplifiedUniversal, Unexpanded, State, ExtendedBranch, NewBranch,
ExtendedEventualities, NewEventualities, ODT_RL, ODT)
).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 4th argument not used.
search_state_aux(_, _, _, _, State,
[pr(State,FmlList)|Branch], [EqualStates,pr(State,FmlList)|Branch],
ExtendedEventualities, ExtendedEventualities, IDT, IDT) :-
pdl_write_ln('In search_state_aux (1)....'),
pdl_write(' State : '), pdl_write(State), pdl_nl,
pdl_write(' FmlList : '), pdl_write(FmlList), pdl_nl,
pdl_write(' Branch : '), pdl_write(Branch), pdl_nl,
is_copy(FmlList, State, Branch, EqualStates), !.
search_state_aux(Axioms, SimplifiedExistential, SimplifiedUniversal,
_, State, ExtendedBranch, NewBranch,
ExtendedEventualities, NewEventualities, IDT, ODT) :-
% pdl_write_ln('In search_state_aux (2)....'),
reduce_existentials(Axioms, SimplifiedExistential, State,
SimplifiedUniversal, ExtendedBranch, NewBranch,
ExtendedEventualities, NewEventualities, IDT, ODT).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% extend_branch(+State, +FmlList, +Branch, -ExtendedBranch)
extend_branch(State, FmlList, Branch, [pr(State, FmlList)|Branch]).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% The key proof_steps_counter counts the proof steps
set_proof_steps_counter(Number) :- !,
pdl_write('set_proof_steps_counter to '), pdl_write(Number), pdl_nl,
flag(proof_steps_counter, _, Number).
increment_proof_steps_counter(Increment) :- !,
flag(proof_steps_counter, Old, Old + Increment).
get_proof_steps_counter(Number) :- !,
flag(proof_steps_counter, Number, Number).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% The key states_counter counts the states created
set_states_counter(Number) :- !,
pdl_write('set_states_counter to '), pdl_write(Number), pdl_nl,
flag(states_counter, _, Number).
increment_states_counter(Increment) :- !,
flag(states_counter, Old, Old + Increment).
get_states_counter(Number) :- !,
flag(states_counter, Number, Number).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% The key branch_point_counter counts the branch_points
set_branch_point_counter(Number) :- !,
pdl_write('set_branch_point_counter to '), pdl_write(Number), pdl_nl,
flag(branch_point_counter, _, Number).
increment_branch_point_counter(Increment) :- !,
flag(branch_point_counter, Old, Old + Increment).
get_branch_point_counter(Number) :- !,
flag(branch_point_counter, Number, Number).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% The key sat_reuse_counter counts the number of times a stored
% satisfiable set is re-used
set_sat_reuse_counter(Number) :- !,
pdl_write('set_sat_reuse_counter to '), pdl_write(Number), pdl_nl,
flag(sat_reuse_counter, _, Number).
increment_sat_reuse_counter(Increment) :- !,
flag(sat_reuse_counter, Old, Old + Increment).
get_sat_reuse_counter(Number) :- !,
flag(sat_reuse_counter, Number, Number).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% The key unsat_reuse_counter counts the number of times a stored
% unsatisfiable set is re-used
set_unsat_reuse_counter(Number) :- !,
pdl_write('set_unsat_reuse_counter to '), pdl_write(Number), pdl_nl,
flag(unsat_reuse_counter, _, Number).
increment_unsat_reuse_counter(Increment) :- !,
flag(unsat_reuse_counter, Old, Old + Increment).
get_unsat_reuse_counter(Number) :- !,
flag(unsat_reuse_counter, Number, Number).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% The key satisfiable is used to track satisfiability on the current
% branch.
% -1 means undefined, 0 means unsatisfiable, 1 means satisfiable
set_satisfiable_flag(Value) :-
flag(satisfiable, _, Value).
get_satisfiability_status(Value) :-
flag(satisfiable, Value, Value).
is_satisfiable(_) :-
get_satisfiability_status(1).
is_unsatisfiable(_) :-
get_satisfiability_status(0).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% test_ignorability(+Branch,+FulfilledEventualities)
% According to Definition 7 in (De Giacomo and Massacci, 2001),
% a \pi-completed branch B is ignorable iff there is an eventuality X which
% is not fulfilled. A branch is \pi-completed if (i) all prefixes are
% reduced, i.e. all rules except -rules have been applied, and
% (ii) for every s1 which is not fully reduced there is a pair (s0,S0)
% shorter than (s1,B) s.t. s0 is fully reduced in the segment S0 and s1 is
% a copy of s0 in B.
% The procedure only uses +Branch to determine all the eventualities
% present on the branch. Whether these are fulfilled is then checked against
% +FulfilledEventualities, a list of all eventualities currently fulfilled
% on the branch.
% Note that since distinct X_i and X_j can represent the
% same eventuality, this check requires more than just comparing, say, the
% number of syntactically distinct X_i present on the branch with the number
% of syntactically distinct X_i in +FulfilledEventualities.
% Note also, that we obtain +FulfilledEventualities from reduce_local.
% +FulfilledEventualities will only be correct, as long complement splitting
% is used to deal with X_i = F and as long rules are applied even if one
% of the consequents is present (i.e. the formula F should not subsume F).
test_ignorability(Branch, FulfilledEventualities) :-
eventualities(Branch, Eventualities),
collectCopies(Branch,Copies),
pdl_write_ln('In test_ignorability... '),
pdl_write(' Branch : '), pdl_write(Branch), pdl_nl,
pdl_write(' FulfilledEventualities : '), pdl_write(FulfilledEventualities), pdl_nl,
pdl_write(' Eventualities : '), pdl_write(Eventualities), pdl_nl,
test_ignorability_loop(Eventualities, FulfilledEventualities, Copies, Branch, _NewEventualities, _NewFulfilledEventualities).
test_ignorability_loop(Eventualities, FulfilledEventualities, Copies, Branch, NewEventualities, NewFulfilledEventualities) :-
test_ignorability_aux(Eventualities, FulfilledEventualities, Copies,
NewEventualities1, NewFulfilledEventualities1),
(NewEventualities1 == [] ->
NewEventualities = NewEventualities1,
NewFulfilledEventualities = NewFulfilledEventualities1
;
(NewFulfilledEventualities1 == FulfilledEventualities ->
print_unfulfilled_eventualities(NewEventualities1),
compute_inconsistent_sets(Eventualities,Branch,Copies),
!,
fail
;
test_ignorability_loop(NewEventualities1, NewFulfilledEventualities1, Copies, Branch, NewEventualities, NewFulfilledEventualities)
)
).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% print_unfulfilled_eventualities(+Eventualities)
%
% print a list of eventualities that are not fulfilled on the current branch
print_unfulfilled_eventualities([]) :-
!.
print_unfulfilled_eventualities([ev(State,x(Y,Fml))|Eventualities]) :-
pdl_write('** Ignorable ** - '), pdl_write(ev(State,x(Y,Fml))), pdl_write(' unfulfilled'), pdl_nl,
print_proof_step('post', '** Ignorable **', ['unfulfilled',ev(State,x(Y,Fml))]),
% print_proof_step('post', '** Ignorable/Unsatisfiable **', ['unfulfilled',x(Y,Fml)]),
!,
print_unfulfilled_eventualities(Eventualities).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% compute_inconsistent_sets(+Eventualities, +Branch, +Copies)
%
compute_inconsistent_sets([], _, _) :-
!.
compute_inconsistent_sets([ev(State,x(_Y,_Fml))|Eventualities], Branch, Copies) :-
get_formulae_for_state(State,Branch,FmlList),
memberchk(isCopyOf(State,_),Copies),
store_inconsistent(FmlList),
!,
compute_inconsistent_sets(Eventualities, Branch, Copies).
get_formulae_for_state(State1,[isCopyOf(_,_)|Branch],FmlList) :-
get_formulae_for_state(State1,Branch,FmlList),
!.
get_formulae_for_state(State1,[pr(State1,FmlList)|_Branch],FmlList) :-
!.
get_formulae_for_state(State1,[pr(State2,_FmlList)|Branch],FmlList) :-
State1 \= State2,
get_formulae_for_state(State1,Branch,FmlList),
!.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% test_ignorability_aux(+Eventualities, +FulfilledEventualities, +Copies,
% -NewEventualities, -NewFulfilledEventualities)
% computes -NewEventualities and -NewFulfilledEventualities from
% +Eventualities and +FulfilledEventualities as follows:
% -NewFulfilledEventualities contains all eventualities in +FulfilledEventualities
% plus any eventuality in +Eventualities that can be shown to be fulfilled with
% respect to +FulfilledEventualities and +Copies;
% -NewEventualities contains all eventualities in +Eventualities that cannot be
% shown to be fulfilled with respect to +FulfilledEventualties and +Copies.
test_ignorability_aux([], FulfilledEventualities, _Copies, [], FulfilledEventualities).
test_ignorability_aux([ev(State,Eventuality)|Eventualities], FulfilledEventualities, Copies, NewEventualities, NewFulfilledEventualities) :-
(test_ignorability_aux_fml(ev(State,Eventuality), FulfilledEventualities, Copies) ->
append(FulfilledEventualities,[fulfilled(State,Eventuality)],NewFulfilledEventualities1),
test_ignorability_aux(Eventualities, NewFulfilledEventualities1, Copies, NewEventualities, NewFulfilledEventualities)
;
test_ignorability_aux(Eventualities, FulfilledEventualities, Copies, NewEventualities1, NewFulfilledEventualities),
NewEventualities = [ev(State,Eventuality)|NewEventualities1]
).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% test_ignorability_aux_fml(+Eventuality, +FulfilledEventualities, +Copies)
%
% succeeds if +Eventuality is a fulfilled eventuality. This in turn is the case
% if (a) among +FulfilledEventualities is a syntactically identical eventuality
% which is already db_recorded as being fulfilled on the current branch, or
% (b) among +FulfilledEventualities is an eventuality Eventuality2, db_recorded to
% be fulfilled at a state State2 such that the state State1 at which +Eventuality
% occurs collapsed to State2.
test_ignorability_aux_fml(_, [], _) :-
fail.
test_ignorability_aux_fml(ev(State1,x(Y,Fml)), [fulfilled(State2, x(X,Fml))|_], Copies) :-
(X = Y ->
print_proof_step('post', fulfilled_by(ev(State1,x(Y,Fml)), ev(State2,x(X,Fml))), '[fulfilled]')
;
collapses(State1,State2,Copies),
print_proof_step('post', fulfilled_by(ev(State1,x(Y,Fml)), ev(State2,x(X,Fml))), '[fulfilled]')
).
test_ignorability_aux_fml(Event, [_|FulfilledEventualities], Copies) :-
test_ignorability_aux_fml(Event, FulfilledEventualities, Copies).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% collectCopies(+Branch, -Copies)
%
% whenever a state State1 is identified as a copy of a State2, we db_record that
% fact by adding `isCopyOf(State1,State2)' on a branch. The predice collectCopies
% retrieves all such facts from +Branch and returns it as a list -Copies.
collectCopies([isCopyOf(State1,State2)|Branch],[isCopyOf(State1,State2)|Copies]) :-
!,
collectCopies(Branch,Copies).
collectCopies([_|Branch],Copies) :-
collectCopies(Branch,Copies),
!.
collectCopies([],[]).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% collapses(+State1, +State2, +Copies)
%
% succeeds if +State1 is a copy of +State2 with respect to the information on
% which states are copies of each other contained in +Copies.
collapses(X, Y, Copies) :-
memberchk(isCopyOf(X,Y),Copies).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% test_unsatisfiability(+State, +FmlList, +CompleteFmlList)
%
% test for inconsistency of the list of formulae FmlList;
% - The first rule states that the empty set/list of formulae is not
% inconsistent
% - The second rule covers conditions 1 and 2 of Definition 23 in %
% (De Giacomo and Massacci, 2000) via a inf_closure
% - The third rule covers condition 3 of Definition 23 in
% (De Giacomo and Massacci, 2000)
test_unsatisfiability(_, [], _) :- !.
% The following rule uses condition 3 of Definition 23 in
% (De Giacomo and Massacci, 2000):
% A superset of a \bot-set is a \bot-set.
test_unsatisfiability(State, Fml, _) :-
list_to_ord_set(Fml,OrdFml1),
inconsistent(OrdFml2),
ord_subset(OrdFml2,OrdFml1),
pdl_write('Reused unsatisfiable set '), pdl_write(OrdFml2), pdl_nl,
print_proof_step(State, inconsistent_subset_of(OrdFml2,OrdFml1), '[inconsistent subset]'),
increment_unsat_reuse_counter(1),
!,
fail.
test_unsatisfiability(State, Set, CompleteFmlList) :-
select_fml(Given, Set, SetWithoutGiven),
inf_closure(State, Given, SetWithoutGiven, CompleteFmlList),
test_unsatisfiability(State, SetWithoutGiven, CompleteFmlList).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
select_fml(Fml, [Fml|FmlList], FmlList).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% is_copy(+FmlList, +CurrentState, +Branch).
%
% test if pr(CurrentState, FmlList) is a copy of an earlier state in
% Branch.
is_copy(_,_,[],_) :-
fail.
is_copy(FmlList, State, [isCopyOf(_,_)|Branch], EqualStates) :-
!,
is_copy(FmlList, State, Branch, EqualStates).
is_copy(FmlList, State, [pr(X,FmlListInX)|_],isCopyOf(State,X)) :-
is_prefix(X, State),
% Ignore the first argument in the introduce literals x(_,Fml)
simplify_X(FmlList, SimplifiedFmlList),
simplify_X(FmlListInX, SimplifiedFmlListInX),
% pdl_write_ln('In is_copy... '),
% pdl_write(' SimplifiedFmlList : '), pdl_write(SimplifiedFmlList), pdl_nl,
% pdl_write(' SimplifiedFmlListInX : '), pdl_write(SimplifiedFmlListInX), pdl_nl,
equal_set(SimplifiedFmlList, State, SimplifiedFmlListInX, X), !.
is_copy(FmlList, State, [pr(_,_)|Branch], EqualStates) :-
is_copy(FmlList, State, Branch, EqualStates).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
is_prefix(X, X).
is_prefix(X, ((Y), _)) :-
is_prefix(X,Y).
prefix_to_list(0,[0]) :- !.
prefix_to_list(((X), L, N),List) :-
prefix_to_list(X,List1),
append(List1,[L,N],List),
!.
list_to_prefix([0],(0)) :- !.
list_to_prefix([A,B|List],(Prefix1,L,N)) :-
append(PrefixList,[L,N],[A,B|List]),
list_to_prefix(PrefixList,Prefix1),
!.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
equal_set([], State, [], X) :- !,
% X is a copy of State
print_copies(State, X).
equal_set([Elem|Set1], State, Set2, X) :-
delete(Set2, Elem, Set3),
equal_set(Set1, State, Set3, X).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
eliminate_duplicates(List, SimplifiedList) :- !,
sort(List, SimplifiedList).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% complement(+Fml,-NotFml)
%
% Returns the complement of Fml.
complement(not(A),A) :- !.
complement(A,not(A)) :- !.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% reduce_existentials(+Axioms, +Existential, +State,
% +Universal, +Branch, -NewBranch,
% +Eventualities, -NewEventualities)
%
% - Applies existential, universal and theory rules
%
reduce_existentials(_, [], _, _, Branch, Branch,
Eventualities, Eventualities, IDT, IDT).
reduce_existentials(Axioms, Existential, X, Universal, Branch, NewBranch,
Eventualities, NewEventualities, IDT, ODT) :- !,
% pdl_write('In reduce_existentials, X : '), pdl_write(X), pdl_nl,
% pdl_write(' Existential : '), pdl_write(Existential), pdl_nl,
select(Fml, Existential, ExistentialWithoutFml),
Fml = dia(R,A),
pdl_write('* R = '), pdl_write(R),
% atom(R),
pdl_write_ln('* '),
increment_states_counter(1),
get_states_counter(N),
Y = (X,R,N),
print_proof_step(Y, A, ['dia',Fml]),
% pdl_write('In reduce_existentials, Y : '), pdl_write(Y), pdl_nl,
reduce_universal(Universal, Y, [], Unexpanded),
extend_unexpanded([A], [], Unexpanded, NewUnexpanded),
reduce_existential(Axioms, NewUnexpanded, Y, Branch, NewBranch1,
Eventualities, NewEventualities1, IDT, ODT_RE),
reduce_existentials(Axioms, ExistentialWithoutFml, X, Universal,
NewBranch1, NewBranch, NewEventualities1, NewEventualities, ODT_RE, ODT).
reduce_existential(Axioms, NewUnexpanded, Y, Branch, NewBranch,
Eventualities, NewEventualities, IDT, ODT) :-
search_state(Axioms, NewUnexpanded, Y, Branch, NewBranch,
Eventualities, NewEventualities, IDT, ODT).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
reduce_universal([], _, Unexpanded, Unexpanded).
reduce_universal([not(dia(R,A))|Universal], Y, Unexpanded, NewUnexpanded) :-
% check if Y is an R-successor
Y = (_,R,_), !,
complement(A, NotA),
extend_unexpanded([NotA], [], Unexpanded, NewUnexpanded1,
Y, ['box',not(dia(R,A))]),
reduce_universal(Universal, Y, NewUnexpanded1, NewUnexpanded).
reduce_universal([_|Universal], Y, Unexpanded, NewUnexpanded) :-
reduce_universal(Universal, Y, Unexpanded, NewUnexpanded).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% extend_unexpanded(+FmlList, +Workedoff, +Unexpanded, -NewUnexpanded,
% +X, +Justification)
% - Adds all non-redundant formulae in FmlList to Unexpanded;
% redundancy is evaluated against Workedoff
% - Keeping all expanded formulae in Workedoff has the disadvantage that
% the performance decreases and proofs are longer.
%
% TO DO: Consider ways of reducing this bookkeeping while preserving
% soundness and completeness.
%
extend_unexpanded([], _, Unexpanded, Unexpanded, _, _).
extend_unexpanded([Fml|Rest], Workedoff, Unexpanded, NewUnexpanded, X, Justification) :-
extend_unexpanded_aux(Fml, Workedoff, Unexpanded, Unexpanded1,
X, Justification), !,
extend_unexpanded(Rest, Workedoff, Unexpanded1, NewUnexpanded, X, Justification).
extend_unexpanded_aux(true, _, Unexpanded, Unexpanded,
X, Justification) :-
print_proof_step(X, '-', Justification).
extend_unexpanded_aux(Fml, Workedoff, Unexpanded, [Fml|Unexpanded],
X, Justification) :-
not_redundant(Fml, Workedoff, Unexpanded),
print_proof_step(X, Fml, Justification).
extend_unexpanded_aux(Fml, _, Unexpanded, Unexpanded, X, Justification) :-
print_redundant_step(X, Fml, Justification).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% extend_unexpanded(+FmlList, +Workedoff, +Unexpanded, -NewUnexpanded)
%
% Same as above, but derivation step is not documented
%
extend_unexpanded([], _, Unexpanded, Unexpanded).
extend_unexpanded([Fml|Rest], Workedoff, Unexpanded, NewUnexpanded) :-
extend_unexpanded_aux(Fml, Workedoff, Unexpanded, Unexpanded1), !,
extend_unexpanded(Rest, Workedoff, Unexpanded1, NewUnexpanded).
extend_unexpanded_aux(Fml, Workedoff, Unexpanded, [Fml|Unexpanded]) :-
not_in_set(Fml, Workedoff),
not_in_set(Fml, Unexpanded).
extend_unexpanded_aux(_, _, Unexpanded, Unexpanded) :-
true.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% not_in_set(+Fml, +FmlList)
%
not_redundant(Fml, FmlList1, FmlList2) :-
not_in_set(Fml, FmlList1),
not_in_set(Fml, FmlList2).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% not_in_set(+Fml, +FmlList)
%
not_in_set(Fml, FmlList) :-
\+ member(Fml, FmlList).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% known_consistent(Fmls)
% If Fmls is a subset of a set of formulae which is already known to be
% consistent, then Fmls is also consistent
%
known_consistent(Fmls,BranchForFmls,EventualitiesForFmls) :-
list_to_ord_set(Fmls,OrdFmls1),
consistent(OrdFmls2,BranchForFmls,EventualitiesForFmls),
ord_subset(OrdFmls1,OrdFmls2),
% write('Reused satisfiable set '), print(OrdFmls2), nl,
% write('Reused a satisfiable set '), nl,
print_proof_step(g, consistent_superset_of(OrdFmls2,OrdFmls1), '[consistent superset]'),
increment_sat_reuse_counter(1),
!.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% print_copies(+State, +CopyState)
%
print_copies(State, CopyState) :-
print_proof_step(State, copy_of(State, CopyState), '[loop checking]').
%%print_copies(State, CopyState) :-
%% sprintf_state(StateString, State),
%% string_to_atom(StateString, State1),
%% sprintf_state(CopyStateString, CopyState),
%% swritef(String, 'copy of %w', [CopyStateString]),
%% string_to_atom(String, StringAtom),
%% print_proof_step(State1, StringAtom, 'loop checking').
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
print_result(Result) :-
write('** '), write(Result), write_ln(' **'),
get_search_output_filename(Filename),
append(Filename),
(get_output_format(latex) ->
write('& \\text{** '), write(Result), write_ln(' **}')
;
write('** '), write(Result), write_ln(' **')
),
told.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
print_proof_step(_, [], _) :- !.
print_proof_step(State, [Fml|FmlList], Justification) :- !,
print_proof_step(State, Fml, Justification),
print_proof_step(State, FmlList, Justification).
print_proof_step(State, Conclusion, Justification) :-
increment_proof_steps_counter(1),
get_proof_steps_counter(N),
% print_proof_step_aux(N, State, Conclusion, Justification),
get_search_output_filename(Filename),
append(Filename),
(get_output_format(latex) ->
print_proof_step_latex(N, State, Conclusion, Justification)
;
print_proof_step_aux(N, State, Conclusion, Justification)
),
told.
print_proof_step_aux(N, State, Conclusion, Justification) :-
pdl_writef('%4r. ', [N]),
get_branch_point_counter(Count),
pdl_tab(Count * 4),
print_state(State), pdl_write(' : '),
print_conclusion(Conclusion), pdl_nl,
pdl_write(' '),
% pdl_write(' '),
pdl_write(Justification), pdl_nl.
print_proof_step_latex(N, State, Conclusion, Justification) :-
pdl_write(N), pdl_write('.\\ & '),
get_branch_point_counter(Count),
print_quad(Count),
print_state_latex(State), pdl_write(' {:} '),
print_conclusion_latex(Conclusion), pdl_nl,
pdl_write('\\tag*{$'),
print_justification_latex(Justification), !,
pdl_write('$}'), pdl_nl,
pdl_write('\\\\'), pdl_nl.
print_quad(0).
print_quad(Count) :-
pdl_write('\\quad\\qquad '),
CountDecr is Count - 1,
print_quad(CountDecr).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
print_redundant_step(_, [], _) :- !.
print_redundant_step(State, [Fml|FmlList], Justification) :- !,
print_redundant_step(State, Fml, Justification),
print_redundant_step(State, FmlList, Justification).
print_redundant_step(State, Conclusion, Justification) :-
print_proof_step_aux('-', State, Conclusion, Justification),
get_search_output_filename(Filename),
append(Filename),
(get_output_format(latex) ->
print_proof_step_latex('-', State, Conclusion, Justification)
;
print_proof_step_aux('-', State, Conclusion, Justification)
),
told.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
print_justification_latex(String) :-
atom(String), !,
rule_name_latex(String, LatexString),
pdl_write(LatexString).
print_justification_latex([String|FmlList]) :-
atom(String), !,
rule_name_latex(String, LatexString),
pdl_write(LatexString), pdl_write('{}: '),
print_formula_list_latex(FmlList).
print_justification_latex(Justification) :- !,
pdl_write(Justification).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
rule_name_latex(true, '\\mltop').
rule_name_latex('or-LEFT', '\\text{${\\mlor}$-left}').
rule_name_latex('or-RIGHT', '\\text{${\\mlor}$-right}').
rule_name_latex('or-RIGHT1', '\\text{${\\mlor}$-right1}').
rule_name_latex('or-RIGHT2', '\\text{${\\mlor}$-right2}').
rule_name_latex('and', '\\neg{\\mlor}').
%rule_name_latex('and', '{\\mland}').
rule_name_latex('dia-or-LEFT', '\\text{$\\mldia{\\mlor}{}$-left}').
rule_name_latex('dia-or-RIGHT', '\\text{$\\mldia{\\mlor}{}$-right}').
rule_name_latex('dia-or-RIGHT1', '\\text{$\\mldia{\\mlor}{}$-right1}').
rule_name_latex('dia-or-RIGHT2', '\\text{$\\mldia{\\mlor}{}$-right2}').
rule_name_latex('dia-comp', '\\mldia{\\comp{}{}}{}').
rule_name_latex('dia-star', '\\mldia{\\ast}{}').
rule_name_latex('dia-test', '\\mldia{?}{}').
rule_name_latex('dia', '\\mldia{\\cdot}{}').
rule_name_latex('X-LEFT', '\\text{$X$-left}').
rule_name_latex('X-RIGHT', '\\text{$X$-right}').
rule_name_latex('X-RIGHT1', '\\text{$X$-right1}').
rule_name_latex('X-RIGHT2', '\\text{$X$-right2}').
rule_name_latex('box-or', '\\neg\\mldia{\\mlor}{}').
rule_name_latex('box-comp', '\\neg\\mldia{\\comp{}{}}{}').
rule_name_latex('box-star', '\\neg\\mldia{\\ast}{}').
rule_name_latex('box-test-LEFT', '\\text{$\\neg\\mldia{?}{}$-left}').
rule_name_latex('box-test-RIGHT', '\\text{$\\neg\\mldia{?}{}$-right}').
rule_name_latex('box-test-RIGHT1', '\\text{$\\neg\\mldia{?}{}$-right1}').
rule_name_latex('box-test-RIGHT2', '\\text{$\\neg\\mldia{?}{}$-right2}').
rule_name_latex('box', '\\neg\\mldia{\\cdot}{}').
%rule_name_latex('box-or', '\\mlbox{\\mlor}{}').
%rule_name_latex('box-comp', '\\mlbox{\\comp}{}').
%rule_name_latex('box-star', '\\mlbox{\\ast}{}').
%rule_name_latex('box', '\\mlbox{\\cdot}{}').
rule_name_latex('[theory]', '\\text{theory}').
rule_name_latex('[theory-inst]', '\\text{theory-inst}').
rule_name_latex('[given]', '\\text{given}').
rule_name_latex('[fulfilled]', '\\text{fulfilled}').
rule_name_latex('[loop checking]', '\\text{loop checking}').
rule_name_latex(String, LatexString) :-
swritef(LatexString, '\\\\text{%w}', [String]).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
justification_latex('[given]', 'given').
justification_latex('[fulfilled]', 'fulfilled').
justification_latex('[loop checking]', 'loop checking').
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
print_formula_list_latex([]).
print_formula_list_latex([Fml]) :-
print_formula_latex(Fml).
print_formula_list_latex([Fml|List]) :-
print_formula_latex(Fml),
pdl_write(', '),
print_formula_list_latex(List).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
print_formula_latex(true) :- !,
pdl_write('\\mltop').
print_formula_latex(false) :- !,
pdl_write('\\mlbot').
print_formula_latex(x(Y,Fml)) :- !,
pdl_write('X^{'), print_state(Y), pdl_write('}_{'),
print_formula_latex(Fml), pdl_write('}').
print_formula_latex(ev(State,x(Y,Fml))) :- !,
print_state(State), pdl_write(' {:} '),
pdl_write('X^{'), print_state(Y), pdl_write('}_{'),
print_formula_latex(Fml), pdl_write('}').
print_formula_latex(at(State,Fml)) :- !,
print_state(State), pdl_write(' {:} '),
print_formula_latex(Fml).
print_formula_latex(and(A,B)) :- !,
pdl_write('('),
print_formula_latex(A),
pdl_write(' \\mland '),
print_formula_latex(B),
pdl_write(')').
print_formula_latex(or(A,B)) :- !,
pdl_write('('),
print_formula_latex(A),
pdl_write(' \\mlor '),
print_formula_latex(B),
pdl_write(')').
print_formula_latex(not(A)) :- !,
pdl_write('\\neg '),
print_formula_latex(A).
print_formula_latex(test(A)) :- !,
pdl_write('\\test{'),
print_formula_latex(A),
pdl_write('}').
print_formula_latex(comp(A,B)) :- !,
pdl_write('(\\comp{'),
print_formula_latex(A),
pdl_write('}{'),
print_formula_latex(B),
pdl_write('})').
print_formula_latex(star(A)) :- !,
print_formula_latex(A),
pdl_write('{}^*').
print_formula_latex(dia(R,A)) :- !,
pdl_write('\\mldia{'),
print_formula_latex(R),
pdl_write('}{'),
print_formula_latex(A),
pdl_write('}').
print_formula_latex(box(R,A)) :- !,
pdl_write('\\mlbox{'),
print_formula_latex(R),
pdl_write('}{'),
print_formula_latex(A),
pdl_write('}').
print_formula_latex(A) :- !,
pdl_write('\\textit{'), pdl_write(A), pdl_write('}').
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
latex_output(begin) :- !,
get_search_output_filename(Filename),
append(Filename),
pdl_write_ln('\\begin{align*}'),
told.
latex_output(end) :- !,
get_search_output_filename(Filename),
append(Filename),
pdl_write_ln('\\end{align*}'),
told.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
sprintf_state(String, (X,Y)) :- !,
sprintf_state(XString, X),
sprintf_state(YString, Y),
swritef(String, '%w.%w', [XString, YString]).
sprintf_state(XString,X) :-
string_to_atom(XString, X).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
print_state((X,Y)) :- !,
print_state(X), pdl_write('.'), print_state(Y).
print_state(X) :-
pdl_write(X).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
print_state_latex((X,Y)) :- !,
print_state_latex(X), pdl_write('.'), print_state_latex(Y).
print_state_latex(X) :-
number(X), !,
pdl_write(X).
print_state_latex(X) :- !,
pdl_write('\\textit{'), pdl_write(X), pdl_write('}').
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
print_conclusion(fulfilled_by(Fml1,Fml2)) :- !,
pdl_write('\\ '), pdl_write(Fml1), pdl_write(' fulfilled by '), pdl_write(Fml2).
print_conclusion(copy_of(X,Y)) :- !,
print_state(X), pdl_write(' copy of '), print_state(Y).
print_conclusion(inconsistent_subset_of(X,Y)) :- !,
print_state(X), pdl_write(' is an inconsistent subset of '), print_state(Y).
print_conclusion(consistent_superset_of(X,Y)) :- !,
print_state(X), pdl_write(' is a consistent superset of '), print_state(Y).
print_conclusion(inconsistent_set(X)) :- !,
print_state(X), pdl_write(' is an inconsistent set').
print_conclusion(consistent_set(X)) :- !,
print_state(X), pdl_write(' is an consistent set').
print_conclusion(X) :-
pdl_write(X).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
print_conclusion_latex(fulfilled_by(Fml1,Fml2)) :- !,
pdl_write(' '),
print_formula_latex(Fml1),
pdl_write('\\textit{ fulfilled by }'),
print_formula_latex(Fml2).
print_conclusion_latex(copy_of(X,Y)) :- !,
print_state_latex(X),
pdl_write('\\textit{ copy of }'),
print_state_latex(Y).
print_conclusion_latex(consistent_set(X)) :- !,
pdl_write('\\begin{array}[t]{l}'), pdl_nl,
print_formula_list_latex(X), pdl_write('\\\\ '), pdl_nl,
pdl_write('\\textit{ is a consistent set }'), pdl_nl,
pdl_write('\\end{array}').
print_conclusion_latex(inconsistent_set(X)) :- !,
pdl_write('\\begin{array}[t]{l}'), pdl_nl,
print_formula_list_latex(X), pdl_write('\\\\ '), pdl_nl,
pdl_write('\\textit{ is an inconsistent set }'), pdl_nl,
pdl_write('\\end{array}').
print_conclusion_latex(consistent_superset_of(X,Y)) :- !,
pdl_write('\\begin{array}[t]{l}'), pdl_nl,
print_formula_list_latex(X), pdl_write('\\\\ '), pdl_nl,
pdl_write('\\textit{ is a consistent superset of }\\\\ '), pdl_nl,
print_formula_list_latex(Y), pdl_write('\\\\ '), pdl_nl,
pdl_write(' \\end{array}').
print_conclusion_latex(inconsistent_subset_of(X,Y)) :- !,
pdl_write('\\begin{array}[t]{l}'), pdl_nl,
print_formula_list_latex(X), pdl_write('\\\\ '), pdl_nl,
pdl_write('\\textit{ is an inconsistent subset of }\\\\ '), pdl_nl,
print_formula_list_latex(Y), pdl_write('\\\\ '), pdl_nl,
pdl_write(' \\end{array}').
print_conclusion_latex(X) :-
print_formula_latex(X).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
print_list([]).
print_list([Head|List]) :-
pdl_write(Head),
pdl_write(' '),
print_list(List).