LP, the Larch Prover -- The instantiate command

The instantiate command provides a method of forward inference, which can be used to substitute terms for free variables, or to eliminate universal quantifiers, from facts in LP's logical system.


<instantiate-command> ::= instantiate (<variable> by <term>)+, in <names>


instantiate s2 by s1 \U s1 in setExtensionality
instantiate x by 0, y by 1 in lemmas


The instantiate command substitutes (simultaneously) the specified terms for the named free variables in the named formulas, rewrite rules, and deduction rules; if a named variable does not occur free in a named fact, but is bound by an accessible prenex-universal quantifier in that fact, then that quantifier is eliminated before the substitution is performed. LP automatically changes bound variables in the named facts, if needed, to avoid having them bind (or capture) variables that occur free in the specified terms.

LP normalizes any nonimmune results from an instantiation, discarding those that normalize to true and orienting any resulting formulas into rewrite rules if the automatic-ordering setting is on. The activity and immunity of the results are determined by the current values of the activity and immunity settings. When instantiating a rewrite rule, LP does not use that rule in normalizing the result.