LP, the Larch Prover — Formulas

A formula is boolean-valued term.

Syntax

<formula> ::= <term>

Restriction: the sort of the <term> must be Bool.

Examples

x + s(y) = s(x + y)
x | y <=> \E z (y = x * z)
x < y \/ x = y \/ y < x
x < y => \E z (x < z /\ z < y)

Usage

Users can assert formulas, prove them, or derive them from other formulas by forward inference.

Operationally, LP uses formulas by orienting them (if possible) into a terminating set of rewrite rules. LP also automatically reduces all nonimmune formulas to normal form.

LP automatically rewrites formulas of the form ~p to p = false and formulas of the form ~p = false to p. Furthermore, it uses the following hardwired deduction rules to derive new formulas from existing formulas and rewrite rules.

lp_and_is_true:  when p /\ q    yield  p, q
lp_or_is_false:  when ~(p \/ q) yield  ~p, ~q

LP uses the names of these deduction rules when it reports their application, but they cannot be entered by the user when naming objects.

To display the formulas that LP has not converted into rewrite rules, type display formulas (or dis fo for short).