LP, the Larch Prover -- New features in Release 3.1
The following features have been added to LP since Release 2.4.
The following features behave differently in Release 3.1 than they did in
Support for full first-order logic, not just the universal-existential subset
supported by Release 2.4. See quantifiers.
A simple sort system for describing polymorphic abstractions.
New inference mechanisms
Proofs by well founded induction.
Proofs of conjectures of the form t1 <=> t2, with t1 => t2
and t2 => t1 as subgoals.
Proofs that use deduction rules for backward inference. See apply.
Richer syntactic conventions, such as x[n] and n!, for
operators and terms.
Additional user amenities, for example, enhanced facilities for
naming sets of statements.
New rewrite rule for the boolean operators, namely, ~p <=> ~q -> p <=> q.
Some settings (e.g., the default name prefix) are
now local to proof contexts.
Names such as thmCaseHyp1.1 are reused within non-overlapping proof
LP now attempts to preserve the order of operands in formulas such as
init => c = 1, so that preference is given to ordering equalities in the
direction the user may have intended when these formulas normalize to