LP, the Larch Prover -- New features in Release 3.1
The following features have been added to LP since Release 2.4.
-
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.
The following features behave differently in Release 3.1 than they did in
Release 2.4.
-
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
contexts.
-
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
equations.