LP, the Larch Prover -- Proofs by generalization

The command prove F by generalizing x from t directs LP to prove a formula F by creating a single subgoal in which the unique accessible (explicit or implicit) prenex-universal quantifier over the variable x has been eliminated from F and all occurrences of x bound by that quantifier have been replaced by t.

The command resume by generalizing x from t directs LP to resume the proof of the current conjecture by this method.

This proof method, which eliminates a universal quantifier from a conjecture, is the dual of the fix command, which eliminates an existential quantifier from a fact. It is subject to restrictions on x and t as for the fix command.

This command is unlikely to be used when F contains free variables other than x. When x is the only free variable in F, the only restriction is that t be a constant that does not occur in F or in any fact in LP's logical system. For example, the command

prove \A x (f(x) = c) by generalizing x from d

is allowed when d is a new constant and reduces the proof of the conjecture to establishing the subgoal f(d) = c. See Skolem-constant.