/* 

Propositional calculus.

Since the following system is trivially saturated under ordered resolution
wrt the subterm ordering, the system is local. Hence, the consequence
problem for propositional calculus is in coNP.


*/


predicates( [true, false] ).

true(X) -> true(or(X,Y)).
true(Y) -> true(or(X,Y)).
false(X),false(Y) -> false(or(X,Y)).
true(X),false(X).
false(not(X))==true(X).




precedence( [or,not,true,false] ).
:-sama([]).        % We want saturation by ordered resolution w/o sel.


/*


*/