The meaning of the logical operators is given by the following hardwired rewrite rules.
LP uses these rewrite rules, together with the following, to simplify terms containing logical operators.~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
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.~(~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
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.