%
% fluent.pl: predicates for manipulating fluent terms
%
% Copyright 2008, Ryan Kelly
%
% This file supplies the basic predicates for manipulating and reasoning
% about fluent terms. It shells out to a third-party prover for the
% hard work.
%
% Variables are expected to be actual prolog variables, as this vastly
% increases the simplicity and efficiency of certain operations. It also
% means we need to take extra care in some other areas. In particular,
% we assume that the formula contains the *only* references to those
% variables, so we are free to bind them in simplification and reasoning.
%
% The following predicate is expected to be provided as a 'black box'
% reasoning engine:
%
% entails(Axioms,Conc): Succeeds when Conc is logically entailed by Axioms
%
% Axioms is a list of formulae, and Conc is a formula. The predicate must
% not bind any variables in Conc.
%
%
% Our logical operators are:
%
% P & Q - logical and
% P | Q - logical or
% P => Q - implication
% P <=> Q - equivalence
% ~P - negation
% !([X:T]:P) - universal quantification with typed variables
% ?([X:T]:P) - existential quantification with types variables
% A = B - object equality
% A \= B - object inequality
% knows(A,P) - individual-level knowledge modality
% pknows(E,P) - complex epistemic modality
%
% Epistemic path operators are:
%
% P ; Q - sequence
% P | Q - choice
% ?(P) - test
% !(X:T) - nondet. rebind of a typed variable
% -([X:V]) - set vars to specific values
% P* - iteration
%
% Most of these are native prolog operators so we dont have
% to declare them ourselves. Note that ! and ?
% take a list variables as their first argument - this
% allows more compact quantification over multiple variables.
%
% Also note that variables are always paired with their type in the
% quantifier - while we could probably deduce the type from its use
% in the enclosed formula, having it explicit is oh so much easier.
%
:- op(200,fx,~).
:- op(500, xfy, <=>).
:- op(500, xfy, =>).
:- op(520, xfy, &).
:- op(1200, xfx, :).
:- op(550, fx, !).
:- op(550, fx, ?).
:- op(400, xf, *).
%
% normalize(F,N) - perform some basic normalisations on a formula
%
% This is designed to make formulae easier to reason about. It
% re-arranges orderless terms into a standard order, for example
% the arguments to '=' and the list of variables in a quantification.
% It also simplifies away some trivial tautologies.
%
normalize((A=B),(A=B)) :-
A @< B, !.
normalize((A=B),(B=A)) :-
B @< A, !.
normalize((A=B),true) :-
A == B, !.
normalize((A\=B),(A\=B)) :-
A @< B, !.
normalize((A\=B),(B\=A)) :-
B @< A, !.
normalize((A\=B),false) :-
A == B, !.
normalize(?(X:P),?(Y:Q)) :-
sort(X,Y),
normalize(P,Q), !.
normalize(!(X:P),!(Y:Q)) :-
sort(X,Y),
normalize(P,Q), !.
normalize(~P,~Q) :-
normalize(P,Q), !.
normalize((P1 & Q1),(P2 & Q2)) :-
normalize(P1,P2),
normalize(Q1,Q2), !.
normalize((P1 | Q1),(P2 | Q2)) :-
normalize(P1,P2),
normalize(Q1,Q2), !.
normalize((P1 => Q1),(P2 => Q2)) :-
normalize(P1,P2),
normalize(Q1,Q2), !.
normalize((P1 <=> Q1),(P2 <=> Q2)) :-
normalize(P1,P2),
normalize(Q1,Q2), !.
normalize(knows(A,P),knows(A,Q)) :-
normalize(P,Q), !.
normalize(pknows(E,P),pknows(E,Q)) :-
normalize(P,Q), !.
normalize(pknows0(E,P),pknows0(E,Q)) :-
normalize(P,Q), !.
normalize(P,P).
%
% struct_equiv(P,Q) - two formulae are structurally equivalent,
% basically meaning they are identical up
% to renaming of variables.
%
% struct_oppos(P,Q) - two formulae are structurally opposed,
% making their conjunction a trivial falsehood.
%
struct_equiv(P,Q) :-
is_atom(P), is_atom(Q), P==Q.
struct_equiv(P1 & P2,Q1 & Q2) :-
struct_equiv(P1,Q1),
struct_equiv(P2,Q2).
struct_equiv(P1 | P2,Q1 | Q2) :-
struct_equiv(P1,Q1),
struct_equiv(P2,Q2).
struct_equiv(P1 => P2,Q1 => Q2) :-
struct_equiv(P1,Q1),
struct_equiv(P2,Q2).
struct_equiv(P1 <=> P2,Q1 <=> Q2) :-
struct_equiv(P1,Q1),
struct_equiv(P2,Q2).
struct_equiv(~P,~Q) :-
struct_equiv(P,Q).
struct_equiv(?([] : P),?([] : Q)) :-
struct_equiv(P,Q).
struct_equiv(?([V1:T|Vs1] : P),?([V2:T|Vs2] : Q)) :-
subs(V1,V2,P,P1),
struct_equiv(?(Vs1 : P1),?(Vs2 : Q)).
struct_equiv(!([] : P),!([] : Q)) :-
struct_equiv(P,Q).
struct_equiv(!([V1:T|Vs1] : P),!([V2:T|Vs2] : Q)) :-
subs(V1,V2,P,P1),
struct_equiv(!(Vs1 : P1),!(Vs2 : Q)).
struct_equiv(knows(A,P),knows(A,Q)) :-
struct_equiv(P,Q).
struct_equiv(pknows(E,P),pknows(E,Q)) :-
struct_equiv(P,Q).
struct_equiv(pknows0(E,P),pknows0(E,Q)) :-
struct_equiv(P,Q).
struct_oppos(P,Q) :-
P = ~P1, struct_equiv(P1,Q) -> true
;
Q = ~Q1, struct_equiv(P,Q1) -> true
;
P=true, Q=false -> true
;
P=false, Q=true.
%
% contradictory(F1,F2) - F1 and F2 are trivially contradictory,
% meaning F1 -> ~F2 and F2 -> ~F1
%
contradictory(F1,F2) :-
struct_oppos(F1,F2) -> true
;
free_vars(F1,Vars1), member(V1,Vars1),
free_vars(F2,Vars2), member(V2,Vars2),
V1 == V2,
really_var_given_value(V1,F1,B),
really_var_given_value(V2,F2,C),
(\+ unifiable(B,C,_)) -> true
;
fail.
really_var_given_value(A,B,C):- call(call,var_given_value(A,B,C)).
%
% fml_compare - provide a standard order over formula terms
%
% This allows them to be sorted, have duplicates removed, etc.
% Formula should be normalised before this is applied.
%
fml_compare('=',F1,F2) :-
struct_equiv(F1,F2), !.
fml_compare(Ord,F1,F2) :-
( F1 @< F2 ->
Ord = '<'
;
Ord = '>'
).
%
% contains_var(A,V) - formula A contains variable V
%
% ncontains_var(A,V) - formula A does not contain variable V
%
%
% Since we know that V is a variable, we do this test by making a copy,
% grounding the copied variable, then checking for structural equivalence
% with the original term.
%
contains_var(A,V:_) :-
copy_term(A:V,A2:V2),
V2=groundme,
A \=@= A2.
ncontains_var(A,V:_) :-
copy_term(A:V,A2:V2),
V2=groundme,
A =@= A2.
%
% flatten_op(Op,Terms,Result) - flatten repeated ops into a list
%
% This precicate succeeds when Result is a list of terms from Terms,
% which were joined by the operator Op. Basically allows a tree of
% similar operators such as ((A & B) & (C & (D & E))) to be flattened
% into a list (A,B,C,D,E).
%
% :- index(flatten_op(0,1,0)).
flatten_op(_,[],[]).
flatten_op(O,[T|Ts],Res) :-
%( var(T) ->
% Res = [T|Res2],
% flatten_op(O,Ts,Res2)
( T =.. [O|Args] ->
append(Args,Ts,Ts2),
flatten_op(O,Ts2,Res)
;
Res = [T|Res2],
flatten_op(O,Ts,Res2)
).
%
% flatten_quant(Q,Ts,VarsIn,VarsOut,Body) - flatten nested quantifiers
%
flatten_quant(Q,T,Vars,Vars,T) :-
\+ functor(T,Q,1), !.
flatten_quant(Q,T,Acc,Vars,Body) :-
T =.. [Q,(V : T2)],
append(V,Acc,Acc2),
flatten_quant(Q,T2,Acc2,Vars,Body).
%
% flatten_quant_and_simp(Q,BodyIn,VarsIn,VarsOut,BodyOut)
% - flatten nested quantifiers, and apply simplification
%
% Just like flatten_quant/5 above, but applies simplify/2 to the body
% when it does not match the quantifier, in case its simplification
% does match.
%
flatten_quant_and_simp(Q,T,VarsIn,VarsOut,Body) :-
( T =.. [Q,(V : T2)] ->
append(V,VarsIn,Vars2),
flatten_quant_and_simp(Q,T2,Vars2,VarsOut,Body)
;
simplify1(T,Tsimp),
( Tsimp =.. [Q,(V : T2)] ->
append(V,VarsIn,Vars2),
flatten_quant_and_simp(Q,T2,Vars2,VarsOut,Body)
;
Body = Tsimp, VarsIn = VarsOut
)
).
%
% ismember(Elem,List) - like member/2, but does not bind variables or
% allow backtracking.
%
ismember(_,[]) :- fail.
ismember(E,[H|T]) :-
( E == H ->
true
;
ismember(E,T)
).
%
% vdelete(List,Elem,Result) - like delete/3 but using equivalence rather
% than unification, so it can be used on lists
% of variables
%
vdelete([],_,[]).
vdelete([H|T],E,Res) :-
( E == H ->
vdelete(T,E,Res)
;
Res = [H|T2],
vdelete(T,E,T2)
).
% :- index(vdelete_list(0,1,0)).
vdelete_list(L,[],L).
vdelete_list(L,[H|T],L2) :-
vdelete(L,H,L1),
vdelete_list(L1,T,L2).
%
% indep_of_vars(Vars,P) - P contains none of the vars in the list Vars,
% i.e. it is independent of the vars.
%
indep_of_vars(Vars,P) :-
\+ ( member(X,Vars), contains_var(P,X) ).
%
% var_in_list(Var,VarL) - variable V is in the list VarL
%
var_in_list([],_) :- fail.
var_in_list([H|T],V) :-
( V == H ->
true
;
var_in_list(T,V)
).
%
% pairfrom(L,E1,E2,Rest) - E1 and E2 are a pair of (different) elements
% from L, wile Rest is the rest of the list
%
% Like doing (member(E1,L), member(E2,L)) but more efficient, doesnt match
% E1 and E2 to the same element, and doesnt generate equivalent permutations.
%
pairfrom(L,E1,E2,Rest) :-
pairfrom_rec(L,[],E1,E2,Rest).
pairfrom_rec([H|T],Rest1,E1,E2,Rest) :-
E1 = H, select(E2,T,Rest2), append(Rest1,Rest2,Rest)
;
pairfrom_rec(T,[H|Rest1],E1,E2,Rest).
%
% simplify(+F1,-F2) - simplify a formula
%
% This predicate applies some basic simplification rules to a formula
% to eliminate redundancy and (hopefully) speed up future reasoning.
%
simplify(P,S) :-
normalize(P,Nml),
simplify1(Nml,S1),
fml2nnf(S1,Nnf),
simplify1(Nnf,S).
simplify1(P,P) :-
is_atom(P), P \= (_ = _), P \= (_ \= _).
simplify1(P & Q,S) :-
flatten_op('&',[P,Q],TermsT),
simplify1_conjunction(TermsT,TermsS),
( TermsS = [] ->
S = true
;
% This will remove duplicates, which includes struct_equiv formulae
predsort(fml_compare,TermsS,Terms),
joinlist('&',Terms,S)
).
simplify1(P | Q,S) :-
flatten_op('|',[P,Q],TermsT),
simplify1_disjunction(TermsT,TermsS),
( TermsS = [] ->
S = false
;
% This will remove duplicates, which includes struct_equiv formulae
predsort(fml_compare,TermsS,Terms),
joinlist('|',Terms,S)
).
simplify1(P => Q,S) :-
simplify1(P,Sp),
simplify1(Q,Sq),
(
Sp=false -> S=true
;
Sp=true -> S=Sq
;
Sq=true -> S=true
;
Sq=false -> S=(~Sp)
;
S = (Sp => Sq)
).
simplify1(P <=> Q,S) :-
simplify1(P,Sp),
simplify1(Q,Sq),
(
struct_equiv(P,Q) -> S=true
;
struct_oppos(P,Q) -> S=false
;
Sp=false -> S=(~Sq)
;
Sq=true -> S=Sq
;
Sq=false -> S=(~Sp)
;
Sq=true -> S=Sp
;
S = (Sp <=> Sq)
).
simplify1(~P,S) :-
simplify1(P,SP),
(
SP=false -> S=true
;
SP=true -> S=false
;
SP = ~P2 -> S=P2
;
SP = (A\=B) -> S=(A=B)
;
S = ~SP
).
simplify1(!(Xs:P),S) :-
( Xs = [] -> simplify1(P,S)
;
flatten_quant_and_simp('!',P,Xs,VarsT,Body),
sort(VarsT,Vars),
(
Body=false -> S=false
;
Body=true -> S=true
;
% Remove any useless variables
partition(ncontains_var(Body),Vars,_,Vars2),
( Vars2 = [] ->
S2 = Body
;
% Pull independent components outside the quantifier.
% Both conjuncts and disjuncts can be handled in this manner.
(flatten_op('|',[Body],BTerms), BTerms = [_,_|_] ->
partition(indep_of_vars(Vars),BTerms,Indep,BT2),
% Because we have removed useless vars, BT2 cannot be empty
joinlist('|',BT2,Body2),
( Indep = [] ->
S2=!(Vars2:Body2)
;
joinlist('|',Indep,IndepB),
S2=(!(Vars2:Body2) | IndepB)
)
; flatten_op('&',[Body],BTerms), BTerms = [_,_|_] ->
partition(indep_of_vars(Vars),BTerms,Indep,BT2),
joinlist('&',BT2,Body2),
( Indep = [] ->
S2=!(Vars2:Body2)
;
joinlist('&',Indep,IndepB),
S2=(!(Vars2:Body2) & IndepB)
)
;
S2=!(Vars2:Body)
)
),
S = S2
)).
simplify1(?(Xs:P),S) :-
( Xs = [] -> simplify1(P,S)
;
flatten_quant_and_simp('?',P,Xs,VarsT,Body),
sort(VarsT,Vars),
(
Body=false -> S=false
;
Body=true -> S=true
;
% Remove vars that are assigned a specific value, simply replacing
% them with their value in the Body formula
member(V1:T1,Vars), var_valuated(V1,Body,Body2) ->
vdelete(Vars,V1:T1,Vars2), simplify1(?(Vars2:Body2),S)
;
% Remove any useless variables
partition(ncontains_var(Body),Vars,_,Vars2),
( Vars2 = [] ->
S = Body
;
% Pull independent components outside the quantifier,
% Both conjuncts and disjuncts can be handled in this manner.
(flatten_op('|',[Body],BTerms), BTerms = [_,_|_] ->
partition(indep_of_vars(Vars),BTerms,Indep,BT2),
joinlist('|',BT2,Body2),
( Indep = [] ->
S = ?(Vars2:Body2)
;
joinlist('|',Indep,IndepB),
S = (?(Vars2:Body2) | IndepB)
)
; flatten_op('&',[Body],BTerms), BTerms = [_,_|_] ->
partition(indep_of_vars(Vars),BTerms,Indep,BT2),
joinlist('&',BT2,Body2),
( Indep = [] ->
S = ?(Vars2:Body2)
;
joinlist('&',Indep,IndepB),
S = (?(Vars2:Body2) & IndepB)
)
;
S = ?(Vars2:Body)
)
)
)).
simplify1((A=B),S) :-
(
A == B -> S=true
;
% Utilising the unique names assumption, we can rewrite it to
% a conjunction of simpler equalities by striping functors, or
% to false if the terms will never unify
( unifiable(A,B,Eqs) ->
joinlist('&',Eqs,S1),
normalize(S1,S)
;
S=false
)
).
simplify1((A\=B),S) :-
(
A == B -> S=false
;
% Utilising the unique names assumption, we can rewrite it to
% a disjunction of simpler inequalities by striping functors, or
% to true if the terms will never unify
( unifiable(A,B,Eqs) ->
joinlist('&',Eqs,S1),
normalize(S1,S2),
S = ~S2
;
S = true
)
).
simplify1(knows(A,P),S) :-
simplify1(P,Ps),
( Ps=true -> S=true
; Ps=false -> S=false
; S = knows(A,Ps)
).
simplify1(pknows(E,P),S) :-
simplify_epath(E,Es),
simplify1(P,Ps),
( Ps=true -> S=true
; Ps=false -> S=false
; Es=(?false) -> S=true
; Es=(?true) -> S=Ps
; S = pknows(Es,Ps)
).
simplify1(pknows0(E,P),S) :-
simplify_epath(E,Es),
simplify1(P,Ps),
( Ps=true -> S=true
%; Ps=false -> S=false % this may be OK if Es=(?false) but we can't
% always detect such a case
; Es=(?false) -> S=true
; Es=(?true) -> S=Ps
; S = pknows0(Es,Ps)
).
%
% simplify1_conjunction(In,Out) - simplify the conjunction of list of fmls
% simplify1_disjunction(In,Out) - simplify the disjunction of list of fmls
%
simplify1_conjunction(FmlsIn,FmlsOut) :-
maplist(simplify1,FmlsIn,FmlsI1),
simplify1_conjunction_rules(FmlsI1,FmlsI2),
simplify1_conjunction_acc(FmlsI2,[],FmlsOut).
simplify1_conjunction_rules(ConjsI,ConjsO) :-
(pairfrom(ConjsI,C1,C2,Rest), (simplify1_conjunction_rule(C1,C2,C1o,C2o) ; simplify1_conjunction_rule(C2,C1,C2o,C1o)) ->
simplify1_conjunction_rules([C1o,C2o|Rest],ConjsO)
;
ConjsO = ConjsI
).
simplify1_conjunction_rule(C1,C2,C1,C2o) :-
C2 = (C2a | C2b),
( struct_oppos(C1,C2a), C2o=C2b
; struct_oppos(C1,C2b), C2o=C2a
).
simplify1_conjunction_rule(C1,C2,C1,true) :-
C2 = (C2a | C2b),
( struct_equiv(C1,C2a)
; struct_equiv(C1,C2b)
).
simplify1_conjunction_acc([],FmlsAcc,FmlsAcc).
simplify1_conjunction_acc([F|FmlsIn],FmlsAcc,FmlsOut) :-
( member(Eq,FmlsAcc), struct_equiv(F,Eq) ->
F2 = true
; member(Opp,FmlsAcc), struct_oppos(F,Opp) ->
F2 = false
;
F2 = F
),
( F2=true ->
simplify1_conjunction_acc(FmlsIn,FmlsAcc,FmlsOut)
; F2=false ->
FmlsOut=[false]
;
simplify1_conjunction_acc(FmlsIn,[F2|FmlsAcc],FmlsOut)
).
simplify1_disjunction(FmlsIn,FmlsOut) :-
maplist(simplify1,FmlsIn,FmlsI1),
simplify1_disjunction_rules(FmlsI1,FmlsI2),
simplify1_disjunction_acc(FmlsI2,[],FmlsOut).
simplify1_disjunction_rules(DisjI,DisjO) :-
(pairfrom(DisjI,D1,D2,Rest), (simplify1_disjunction_rule(D1,D2,D1o,D2o) ; simplify1_disjunction_rule(D2,D1,D2o,D1o)) ->
simplify1_disjunction_rules([D1o,D2o|Rest],DisjO)
;
DisjO = DisjI
).
simplify1_disjunction_rule(D1,D2,D1,D2o) :-
D2 = (D2a & D2b),
( struct_oppos(D1,D2a), D2o=D2b
; struct_oppos(D1,D2b), D2o=D2a
).
simplify1_disjunction_rule(D1,D2,D1,false) :-
D2 = (D2a & D2b),
( struct_equiv(D1,D2a)
; struct_equiv(D1,D2b)
).
simplify1_disjunction_acc([],FmlsAcc,FmlsAcc).
simplify1_disjunction_acc([F|FmlsIn],FmlsAcc,FmlsOut) :-
( member(Eq,FmlsAcc), struct_equiv(F,Eq) ->
F2 = false
; member(Opp,FmlsAcc), struct_oppos(F,Opp) ->
F2 = true
;
F2 = F
),
( F2=false ->
simplify1_disjunction_acc(FmlsIn,FmlsAcc,FmlsOut)
; F2=true ->
FmlsOut=[true]
;
simplify1_disjunction_acc(FmlsIn,[F2|FmlsAcc],FmlsOut)
).
%
% var_given_value(X,P,V,Q) - variable X is uniformly given the value V
% within the formula P. Q is a formula equiv
% to P, with variable X set to V.
%
% var_given_value_list(X,Ps,V,Qs) - variable X is uniformly given the value
% V in all formulae in list Ps.
%
% Determining Q from P is not a simple substitution - if the value V
% contains vars that are introduced by a quantifier in P, this quantifier
% must be lifted to outermost scope.
%
/*
% :- index(var_given_value(0,1,0,0)).
% :- index(var_given_value_list(0,1,0,0)).
*/
var_given_value(X,A=B,V,true) :-
( X == A ->
V = B
;
X == B, V = A
).
var_given_value(X,P1 & P2,V,Q) :-
flatten_op('&',[P1,P2],Cjs),
select(Cj,Cjs,Rest), var_given_value(X,Cj,V,Qj),
partition(vgv_partition(X),Rest,Deps,Indeps),
(Indeps = [] -> IndepFml=true ; joinlist('&',Indeps,IndepFml)),
(Deps = [] -> DepFml1=true ; joinlist('&',Deps,DepFml1)),
subs(X,V,DepFml1,DepFml),
% We may have lifted a variable outside the scope of its
% quantifier. We must push QRest back down through the quantifiers
% to rectify this. By invariants of the operation, we know all
% relevant quantifiers are at outermost scope in Qj.
(DepFml \= true ->
term_variables(V,Vars),
vgv_push_into_quantifiers(Vars,Qj,DepFml,QFml)
;
QFml = Qj
),
Q = (IndepFml & QFml), !.
var_given_value(X,P1 | P2,V,Q) :-
flatten_op('|',[P1,P2],Djs),
var_given_value_list(X,Djs,V,Qs),
joinlist('|',Qs,Q).
var_given_value(X,!(Vars:P),V,!(VarsQ:Q)) :-
var_given_value(X,P,V,Q2),
flatten_quant('!',Q2,Vars,VarsQ,Q).
var_given_value(X,?(Vars:P),V,?(VarsQ:Q)) :-
var_given_value(X,P,V,Q2),
flatten_quant('?',Q2,Vars,VarsQ,Q).
var_given_value(X,knows(A,P),V,knows(A,Q)) :-
var_given_value(X,P,V,Q).
var_given_value(X,pknows(E,P),V,pknows(E,Q)) :-
var_given_value(X,P,V,Q).
var_given_value(X,pknows0(E,P),V,pknows0(E,Q)) :-
var_given_value(X,P,V,Q).
% There's no clause for ~P because that can never give X a specific value
var_given_value_list(_,[],_,[]).
var_given_value_list(X,[H|T],V,[Qh|Qt]) :-
% Be careful not to do any unification on V.
% This ruins tail-recursion, but meh...
var_given_value(X,H,V,Qh),
var_given_value_list(X,T,V2,Qt),
V == V2.
vgv_partition(V,F) :-
contains_var(F,V:_).
% We can stop recursing either when Vars=[] or when we are
% no longer at a quantifier, since we assume all relevant
% quantifiers have been brought to the front.
vgv_push_into_quantifiers(Vars,?(Qv:Qj),QDep,?(Qv:Q)) :-
Vars \= [], !,
vgv_subtract(Vars,Qv,Vars2),
vgv_push_into_quantifiers(Vars2,Qj,QDep,Q).
vgv_push_into_quantifiers(Vars,!(Qv:Qj),QDep,!(Qv:Q)) :-
Vars \= [], !,
vgv_subtract(Vars,Qv,Vars2),
vgv_push_into_quantifiers(Vars2,Qj,QDep,Q).
vgv_push_into_quantifiers(_,Qj,QDep,Qj & QDep).
vgv_subtract([],_,[]).
vgv_subtract(Vs,[],Vs).
vgv_subtract(Vs,[X:_|Xs],Vs2) :-
vgv_subtract_helper(Vs,X,Vs1),
vgv_subtract(Vs1,Xs,Vs2).
vgv_subtract_helper([],_,[]).
vgv_subtract_helper([V|Vs],X,Vs2) :-
( X == V ->
vgv_subtract_helper(Vs,X,Vs2)
;
Vs2 = [V|Vs22],
vgv_subtract_helper(Vs,X,Vs22)
).
%
% var_valuated(X,P,P2) - variable X takes specific values throughout P,
% and P2 is P with the appropriate valuations
% inserted.
%
% :- index(var_valuated(0,1,0)).
% :- index(var_valuated_list(0,1,0)).
% :- index(var_valuated_distribute(0,1,0,0)).
% In the base case, X is given a single value throughout the entire formula.
var_valuated(X,P,Q) :-
var_given_value(X,P,_,Q), !.
% The base case for P & Q - when they both give X the same value - is
% already covered by the var_valuated/3 clause above. But if one of the
% conjuncts is a disjunction that valuates X, then we can distribute over
% it to achieve a valuation.
var_valuated(X,P & Q,V) :-
flatten_op('&',[P,Q],Cjs),
select(Cj,Cjs,RestCjs),
flatten_op('|',[Cj],Djs),
maplist(var_valuated_check(X),Djs), !,
joinlist('&',RestCjs,RestFml),
var_valuated_distribute(X,Djs,RestFml,VDjs),
joinlist('|',VDjs,V), !.
var_valuated(X,P | Q,V) :-
flatten_op('|',[P,Q],Cs),
var_valuated_list(X,Cs,Vs),
joinlist('|',Vs,V).
var_valuated(X,!(V:P),!(V:Q)) :-
var_valuated(X,P,Q).
var_valuated(X,?(V:P),?(V:Q)) :-
var_valuated(X,P,Q).
var_valuated_list(_,[],[]).
var_valuated_list(X,[H|T],[Hv|Tv]) :-
var_valuated(X,H,Hv),
var_valuated_list(X,T,Tv).
var_valuated_distribute(_,[],_,[]).
var_valuated_distribute(X,[P|Ps],Q,[Pv|T]) :-
var_valuated(X,P & Q,Pv),
var_valuated_distribute(X,Ps,Q,T).
var_valuated_check(X,F) :-
%var_valuated(X,F,_).
var_given_value(X,F,_,_).
%
% joinlist(+Op,+In,-Out) - join items in a list using given operator
%
joinlist(_,[H],H) :- !.
joinlist(O,[H|T],J) :-
T \= [],
J =.. [O,H,TJ],
joinlist(O,T,TJ).
%
% subs(Name,Value,Old,New): substitue values in a term
%
% This predicate is true when New is equal to Old with all occurances
% of Name replaced by Value - basically, a symbolic substitution
% routine. For example, it is usually used to produce a result such
% as:
%
% subs(now,S,fluent(now),fluent(S)).
%
subs(X,Y,T,Tr) :-
T == X, Tr = Y, !.
subs(X,_,T,Tr) :-
T \== X, var(T), T=Tr, !.
subs(X,Y,T,Tr) :-
T \== X, nonvar(T), T =.. [F|Ts], subs_list(X,Y,Ts,Trs), Tr =.. [F|Trs], !.
%
% subs_list(Name,Value,Old,New): value substitution in a list
%
% This predicate operates as subs/4, but Old and New are lists of terms
% instead of single terms. Basically, it calls subs/4 recursively on
% each element of the list.
%
subs_list(_,_,[],[]).
subs_list(X,Y,[T|Ts],[Tr|Trs]) :-
subs(X,Y,T,Tr), subs_list(X,Y,Ts,Trs).
%
% fml2nnf: convert a formula to negation normal form
%
fml2nnf(P <=> Q,N) :-
fml2nnf((P => Q) & (Q => P),N), !.
fml2nnf(P => Q,N) :-
fml2nnf((~P) | Q,N), !.
fml2nnf(~(P <=> Q),N) :-
fml2nnf(~(P => Q) & ~(Q => P),N), !.
fml2nnf(~(P => Q),N) :-
fml2nnf(P & ~Q,N), !.
fml2nnf(~(P & Q),N) :-
fml2nnf((~P) | (~Q),N), !.
fml2nnf(~(P | Q),N) :-
fml2nnf((~P) & (~Q),N), !.
fml2nnf(~(!(X:P)),N) :-
fml2nnf( ?(X : ~P) ,N), !.
fml2nnf(~(?(X:P)),N) :-
fml2nnf(!(X : ~P),N), !.
fml2nnf(~(~P),N) :-
fml2nnf(P,N), !.
fml2nnf(P & Q,Np & Nq) :-
fml2nnf(P,Np), fml2nnf(Q,Nq), !.
fml2nnf(P | Q,Np | Nq) :-
fml2nnf(P,Np), fml2nnf(Q,Nq), !.
fml2nnf(!(X:P),!(X:N)) :-
fml2nnf(P,N), !.
fml2nnf(?(X:P),?(X:N)) :-
fml2nnf(P,N), !.
fml2nnf(knows(A,P),knows(A,N)) :-
fml2nnf(P,N), !.
fml2nnf(pknows(E,P),pknows(E,N)) :-
fml2nnf(P,N), !.
fml2nnf(pknows0(E,P),pknows0(E,N)) :-
fml2nnf(P,N), !.
fml2nnf(~knows(A,P),~knows(A,N)) :-
fml2nnf(P,N), !.
fml2nnf(~pknows(E,P),~pknows(E,N)) :-
fml2nnf(P,N), !.
fml2nnf(~pknows0(E,P),~pknows0(E,N)) :-
fml2nnf(P,N), !.
fml2nnf(P,P).
%
% is_atom(P) - the formula P is a literal atom, not a compound expression
%
% This is used to detect the base case of many predicates that structurally
% decompose formulae.
%
is_atom(P) :-
P \= (~_),
P \= (_ => _),
P \= (_ <=> _),
P \= (_ & _),
P \= (_ | _),
P \= ?(_:_),
P \= !(_:_),
P \= knows(_,_),
P \= pknows(_,_),
P \= pknows0(_,_).
%
% copy_fml(P,Q) - make a copy of a formula. The copy will have all
% bound variables renamed to new vars. Any free variables
% will retain their original names.
%
copy_fml(P,P) :-
var(P), !.
copy_fml(P,P) :-
is_atom(P).
copy_fml(P & Q,R & S) :-
copy_fml(P,R),
copy_fml(Q,S).
copy_fml(P | Q,R | S) :-
copy_fml(P,R),
copy_fml(Q,S).
copy_fml(P => Q,R => S) :-
copy_fml(P,R),
copy_fml(Q,S).
copy_fml(P <=> Q,R <=> S) :-
copy_fml(P,R),
copy_fml(Q,S).
copy_fml(~P,~Q) :-
copy_fml(P,Q).
copy_fml(!(VarsP:P),!(VarsQ:Q)) :-
rename_vars(VarsP,P,VarsQ,P2),
copy_fml(P2,Q).
copy_fml(?(VarsP:P),?(VarsQ:Q)) :-
rename_vars(VarsP,P,VarsQ,P2),
copy_fml(P2,Q).
copy_fml(knows(A,P),knows(A,Q)) :-
copy_fml(P,Q).
copy_fml(pknows(E,P),pknows(F,Q)) :-
copy_epath(E,F),
copy_fml(P,Q).
copy_fml(pknows0(E,P),pknows0(F,Q)) :-
copy_epath(E,F),
copy_fml(P,Q).
%
% rename_vars(Vars,F,NewVars,NewF) - rename the given variables to new
% ones, producing a modified formula.
%
rename_vars(Vs,P,Vs2,P2) :-
rename_vars(Vs,P,[],Vs2,P2).
rename_vars([],P,Acc,Acc,P).
rename_vars([V:T|Vs],P,Acc,NewV,NewP) :-
subs(V,V2,P,P2),
append(Acc,[V2:T],Acc2),
rename_vars(Vs,P2,Acc2,NewV,NewP).
%
% free_vars(Fml,Vars) - list of all free variables in the formula
%
% "Free" is in the FOL sense of "not bound by an enclosing quantifier"
%
free_vars(Fml,Vars) :-
copy_fml(Fml,Fml2),
term_variables(Fml,Vars1),
term_variables(Fml2,Vars2),
vars_in_both(Vars1,Vars2,[],Vars).
vars_in_both([],_,Vars,Vars).
vars_in_both([H|T],V2,Acc,Vars) :-
( ismember(H,V2) ->
vars_in_both(T,V2,[H|Acc],Vars)
;
vars_in_both(T,V2,Acc,Vars)
).
write_eqn(P) :-
write('\\begin{multline}'),nl,write_latex(P),nl,write('\\end{multline}').
write_latex(P) :-
copy_fml(P,Pc),
number_vars(Pc),
do_write_latex(Pc).
do_write_latex(P) :-
var(P), write(P), !.
do_write_latex(P <=> Q) :-
do_write_latex(P), write(' \\equiv '), do_write_latex(Q).
do_write_latex(P => Q) :-
do_write_latex(P), write(' \\rightarrow '), do_write_latex(Q).
do_write_latex(~P) :-
write(' \\neg '), do_write_latex(P).
do_write_latex(P & Q) :-
flatten_op('&',[P & Q],[C|Cs]),
write(' \\left( '), do_write_latex(C), reverse(Cs,CsR),
do_write_latex_lst(CsR,' \\wedge '), write(' \\right) ').
do_write_latex(P | Q) :-
flatten_op('|',['|'(P,Q)],[C|Cs]),
do_write_latex(C), reverse(Cs,CsR),
do_write_latex_lst(CsR,' \\vee ').
do_write_latex(!([X|Xs]:P)) :-
write(' \\forall '),
do_write_latex(X),
do_write_latex_lst(Xs,','),
write(' : \\left[ '),
do_write_latex(P),
write(' \\right] ').
do_write_latex(?([X|Xs]:P)) :-
write(' \\exists '),
do_write_latex(X),
do_write_latex_lst(Xs,','),
write(' : \\left[ '),
do_write_latex(P),
write(' \\right] ').
do_write_latex(knows(A,P)) :-
write(' \\Knows( '),
do_write_latex(A),
write(','),
do_write_latex(P),
write(')').
do_write_latex(pknows(E,P)) :-
write(' \\PKnows( '),
do_write_latex(E),
write(','),
do_write_latex(P),
write(')').
do_write_latex(P) :-
is_atom(P), write(P).
do_write_latex_lst([],_).
do_write_latex_lst([T|Ts],Sep) :-
write(Sep), nl, do_write_latex(T), do_write_latex_lst(Ts,Sep).
number_vars(X) :-
term_variables(X,Vs),
number_vars_rec(Vs,0).
number_vars_rec([],_).
number_vars_rec([V|Vs],N) :-
name(x,N1), name(N,N2), append(N1,N2,Codes),
atom_codes(V,Codes),
Ns is N + 1,
number_vars_rec(Vs,Ns).
%
% pp_fml(P) - pretty-print the formula P
%
pp_fml(P) :-
copy_fml(P,F), fml2nnf(F,N), number_vars(N),
pp_fml(N,0,0), !, nl, nl.
pp_inset(0).
pp_inset(N) :-
N > 0, N1 is N - 1,
write(' '), pp_inset(N1).
pp_fml_list([P],_,_,O1,D1) :-
pp_fml(P,O1,D1).
pp_fml_list([P1,P2|Ps],Op,D,O1,D1) :-
pp_fml(P1,O1,D1), nl,
pp_inset(D), write(Op), nl,
pp_fml_list([P2|Ps],Op,D,D1,D1).
pp_fml(P1 & P2,O,D) :-
flatten_op('&',[P1,P2],Ps),
D1 is D + 1,
O1 is O + 1,
pp_fml_list(Ps,'&',D,O1,D1).
pp_fml(P1 | P2,O,D) :-
flatten_op('|',[P1,P2],Ps),
D1 is D + 1,
O1 is O + 1,
pp_fml_list(Ps,'|',D,O1,D1).
pp_fml(~P,O,D) :-
D1 is D + 1,
pp_inset(O), write('~ '),
pp_fml(P,0,D1).
pp_fml(P1 => P2,O,D) :-
D1 is D + 1,
pp_inset(O), pp_fml(P1,1,D1), nl,
pp_inset(D), write('=>'), nl,
pp_fml(P2,D1,D1).
pp_fml(P1 <=> P2,O,D) :-
D1 is D + 1,
pp_inset(O), pp_fml(P1,1,D1), nl,
pp_inset(D), write('<=>'), nl,
pp_fml(P2,D1,D1).
pp_fml(!(V:P),O,D) :-
D1 is D + 1,
pp_inset(O), write('!('), write(V), write('):'), nl,
pp_fml(P,D1,D1).
pp_fml(?(V:P),O,D) :-
D1 is D + 1,
pp_inset(O), write('?('), write(V), write('):'), nl,
pp_fml(P,D1,D1).
pp_fml(knows(A,P),O,D) :-
D1 is D + 1,
pp_inset(O), write('knows('), write(A), write(','), nl,
pp_fml(P,D1,D1), nl,
pp_inset(D), write(')').
pp_fml(pknows(E,P),O,D) :-
D1 is D + 1,
pp_inset(O), write('pknows('), nl,
pp_epath(E,D1,D1), nl,
pp_inset(D), write('-----'), nl,
pp_fml(P,D1,D1), nl,
pp_inset(D), write(')').
pp_fml(pknows0(E,P),O,D) :-
D1 is D + 1,
pp_inset(O), write('pknows0('), nl,
pp_epath(E,D1,D1), nl,
pp_inset(D), write('-----'), nl,
pp_fml(P,D1,D1), nl,
pp_inset(D), write(')').
pp_fml(P,O,_) :-
is_atom(P),
pp_inset(O), write(P).
fml2cnf(P,P) :-
is_atom(P).
fml2cnf(P1 & P2,C1 & C2) :-
fml2cnf(P1,C1),
fml2cnf(P2,C2).
fml2cnf(P1 | P2,C) :-
fml2cnf(P1,C1),
fml2cnf(P2,C2),
flatten_op('&',[C1],C1s),
flatten_op('&',[C2],C2s),
setof(Cp,fml2cnf_helper(C1s,C2s,Cp),Cs),
joinlist('&',Cs,C).
fml2cnf_helper(Cjs1,Cjs2,C) :-
member(C1,Cjs1), member(C2,Cjs2), C = (C1 | C2).
:- begin_tests(fluent,[sto(rational_trees)]).
test(simp1) :-
simplify(p & true,p).
test(simp2) :-
simplify(p & false,false).
test(simp3) :-
simplify(p | false,p).
test(simp4) :-
simplify(p | true,true).
test(simp5) :-
simplify(false | false,false).
test(simp6) :-
simplify(false | (p & ~(a=a)),false).
test(simp7) :-
simplify(true & true,true).
test(simp8) :-
simplify(!([X:t]: p(X) & p(a)),!([X:t]:p(X)) & p(a)).
test(simp9) :-
simplify(?([X:t]: p(X) & p(a)),?([X:t]:p(X)) & p(a)).
test(simp10) :-
X1 = ?([X:t] : ((p & (X=nil)) | (q & (X=obs) & r ) | (?([Y:o]:(s(Y) & (X=pair(a,Y))))))),
X2 = (p | ?([Y:o] : s(Y)) | (q & r)),
simplify(X1,X2).
test(val1) :-
var_given_value(X,X=a,a,true).
test(val2) :-
var_given_value(X,(X=a) & (X=b),b,F), simplify(F,false).
test(val3) :-
var_given_value(X,p(X) & q(a) & ?([Y:t]:X=Y),Val,_),
Val == Y.
test(copy1) :-
F1 = !([X:t,Y:q] : p(X) & r(Y)),
copy_fml(F1,F2),
F1 =@= F2,
F1 \== F2.
:- end_tests(fluent).