predicates( [r,-] ).

% World = 1st argument


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

P-W -> '$or'(P,Q)-W.
Q-W -> '$or'(P,Q)-W.
'$or'(P,Q)-W -> P-W, Q-W.
P-W, '$not'(P)-W.
P-W, '$not'(P)-W -> [].

'$diam'(P)-X -> P-g(P,X).
'$diam'(P)-X -> r(X,g(P,X)).
r(X,W), P-W -> '$diam'(P)-X.
'$box'(P)= '$not'('$diam'('$not'(P))).


'$and'(P,Q)='$not'('$or'('$not'(P),'$not'(Q))).
'$impl'(P,Q)='$or'('$not'(P),Q).
'$equiv'(P,Q)='$and'('$impl'(P,Q),'$impl'(Q,P)).
'$not'('$not'(P))=P.

first_predicate_precedence([-]).
precedence( [g,h,f,'$box','$diam','$equiv','$impl','$and','$or','$var','$not',r,p,q,w] ).

%:-option(term_var_size).
%:-sama([2]).