/* 
That this can be finitely saturated under the subterm ordering
proves that the satisfiability probl;em for KD45 is in NP.
*/


predicates( [r,-] ).


% World = 2nd argument of -


% result of saturating the KD45 background theory
r(B,f(C,D)).
r(B,C),'$min'=C.
r(B,C) -> r(D,C).

% propositional logic for expressions in negation normal form:
% we need negation just for variables

P-W -> '$or'(P,Q)-W.
Q-W -> '$or'(P,Q)-W.
'$or'(P,Q)-W -> P-W, Q-W.
P-W, Q-W -> '$and'(P,Q)-W.
'$and'(P,Q)-W -> P-W.
'$and'(P,Q)-W -> Q-W.

% negation just for variables
'$var'(P)-W, '$var'('$not'(P))-W.
'$var'(P)-W, '$var'('$not'(P))-W -> [].
'$not'('$not'(P)) = P.


/*
For KD45 it suffices to have box and diamond applied to prop variables
as we have the following identities (modulo AC of disjunction):

 box(not(P)) = not(diam(P)).
diam(not(P)) =  not(box(P)).

box(or(P,diam(Q))) = or(box(P),diam(Q)).  (cf. th12 and th22)
box(or(P,box(Q)))  = or(box(P),box(Q)).
% similar for conjunctions via DeMorgan	

Moreover we assume that both
box and diamond occur only negatively in goals,
i.e., positively in the theorems that we want to prove,
so that we need just one direction of the respective definitions.

*/


'$diam'('$var'(P))-X        -> '$var'(P)-f(X,g('$var'(P),X)).
'$box'('$var'(P))-X, r(X,W) -> '$var'(P)-W.


precedence( [g,f,'$diam','$box','$or','$and','$var','$not',-,r,w] ).
:-ordering(sto).
:-sama([]).        % We want saturation by ordered resolution w/o sel.