LP, the Larch Prover -- Logical operators

Syntax

LP automatically declares the sort Bool and the following logical operators.
true
A constant denoting the value true of sort Bool.
false
A constant denoting the value false of sort Bool.
~
A prefix operator, pronounced ``not'', denoting negation.
/\
An infix operator, pronounced ``and'', denoting conjunction.
\/
An infix operator, pronounced ``or'', denoting disjunction.
=>
An infix operator, pronounced ``implies'', denoting implication.
<=>
An infix operator, pronounced ``if and only if'', denoting equivalence. The operator <=> is a synonym for the equality operator =:Bool,Bool->Bool; it differs from = only in that it binds less tightly during parsing.

Semantics

LP treats /\, \/, and <=> as associative-commutative operators.

The meaning of the logical operators is given by the following hardwired rewrite rules. 

~true      -> false               true => p   -> p
~false     -> true                false => p  -> true
                                  p => true   -> true
p /\ true  -> p                   p => false  -> ~p
p /\ false -> false  
             
p \/ true  -> true                p <=> false -> ~p
p \/ false -> p                   p <=> true  -> p
LP uses these rewrite rules, together with the following, to simplify terms containing logical operators. 
~(~p)      -> p                   p => p      -> true
                                  p => ~p     -> ~p
p /\ p     -> p                   ~p => p     -> p
p /\ ~p    -> false
                                  p <=> p     -> true
p \/ p     -> p                   p <=> ~p    -> false
p \/ ~p    -> true                ~p <=> ~q   -> p <=> q
These rewrite rules are not sufficient to reduce all boolean tautologies to true. There are sets of rewrite rules that are complete in this sense, but they require exponential time and space, and they can expand rather than simplify expressions that do not reduce to true or false. Hence they are not hardwired into LP. Users wishing to use such a set can execute the file ~lp/boolequiv.lp or the file ~lp/boolxor.lp.

To assist in orienting formulas into rewrite rules, LP places true and false at the bottom of the registry, and it registers /\, \/, and <=> as having multiset status.

See also