LP, the Larch Prover — The apply command

The apply command provides manual control over the application of (possibly passive) deduction rules to (possibly immune) formulas and rewrite rules. It also provides a means of backward inference for finishing the proof of a conjecture.

Syntax

<apply-command> ::= apply <names> to <target>
<target>        ::= <names> | conjecture

Examples

apply passive / deduction-rules to *
apply setExtensionality to conjecture

Usage

The first version of the apply command applies the named deduction rules, whether or not they are active, to the formulas and rewrite rules named as the <target>, whether or not they are immune.

The second version attempts to prove the current conjecture by explicit deduction using the named deduction rules. The attempt succeeds if the current conjecture matches a conclusion of a named deduction rule and the hypotheses of that deduction rule, under the matching substitution, reduce to true. For example, if LP's logical system contains the axioms

setAxioms.1:         e \in (x \U y) -> e \in x \/ e \in y
setExtensionality.1: when \A e (e \in s1 <=> e \in s2) yield s1 = s2

then the command apply setExtensionality to conjecture finishes the proof of the conjecture x \U x = x.