/*
This is an encoding of the modal logic KD45.

KD45 has the following axioms:

K: box(A -> B) -> (box A -> box B)
D: box A -> diam A
4: box A -> box box A
5: diam A -> box diam A

together with the standard inference
  A
-----  .
box A

In the emcoding,
r is the accessibility relation of its Kripke
semantics.
r is also represented by a family of functions f_x, coded as 
a binary function f(_,x).
More exactly, 
 
     r(U,V) = exist x: f(U,x) = V.

This is possible because of D which implies diam true,
hence that every world accesses some other world.
Otherwise the functions f_x would have to be partial.


Saturation terminates with finding, essentially,
	r(x1,f(x2,x3)).

``*'' in the final set of clauses denotes cases in which the first
literal in the antecedent has been selected for superposition.
These clauses are redundant in any extension in which no
new clauses with positive occurrences of r are present.
In such cases the only remaining inferences are those with

         -> r(x1,f(x2,x3))
         -> r(x1,x2),$min=x2

Additional positive occurrences of r are avoided by coding

     (box A)_u    as  all v: r(u,v) -> A_v

and

     (diam A)_u   as  exists x: A_f(u,x)

and by using the equivalence box A <-> not diam not A.

Without using the smallest constant '$min' explicitly we 
obtain the additional disjunction

          -> x1=x2,r(x3,x1),r(x4,x2).

Also, this case seems to produce complex constraints
and can be saturated only with saci([]).


*/

:-option(special_relations(off)).


'-p'(U,V), '-p'(V,W) -> '-p'(U,W).    % 4

'-p'(U,V), '-p'(U,W) -> '-p'(V,W).    % 5

%f(U,X)=V -> '-p'(U,V).          % functional coding is made possible by D
'-p'(U,f(U,X)).          % functional coding is made possible by D

axiom([[],['-p'('$min',U)],[[[U>'$min'],[]]]]).
        

	% for refutational theorem proving
	% one may restrict oneselves to the reachable worlds from
	% some initial world denoted '$min'


'+p'(U,V) -> '-p'(U,V).

:-option([term_size_weight]).


:-sama([]).
:-sarp([1,2,3,4,6,7,10]),sams([3,19]),saci([2]).
:-option(crw_depth(1)).



/*

*/