Major Section: RULE-CLASSES
See rule-classes for a general discussion of rule classes and
how they are used to build rules from formulas. An example
corollary formula from which a
:generalize rule might be built is:
Example: any theoremTo use such a
General Form: any theorem
:generalizerule, the system waits until it has decided to generalize some term,
term, by replacing it with some new variable
v. If any
:generalizeformula can be instantiated so that some non-variable subterm becomes
term, then that instance of the formula is added as a hypothesis.
At the moment, the best description of how ACL2
are used may be found in the discussion of ``Generalize Rules,'' page
248 of A Computational Logic Handbook, or ``Generalization,'' page
132 of ``Computer-Aided Reasoning: An Approach.''