/* 

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)).
true(or(X,Y)) -> true(X),true(Y).
true(X),true(not(X)).
true(X),true(not(X)) -> [].




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


/*


*/