Computing Induction Axioms

Abstract The computation of induction axioms in the explicit induction paradigm is investigated. A simple notion with a well-defined semantics, called a relation description, is proposed as the elementary building block for automated reasoning on induction axioms. It is demonstrated how relation descriptions can be created, manipulated and compared by machine so that useful and strong induction axioms can be derived from them. For each of these operations the semantics of their effects and a precise semantical justification for their application is given. It is shown how the proposed framework can be used to describe the methods implemented in Boyer and Moore's NQTHM system in an abstract setting with a well-defined semantics. NQTHM's merging and subsumption heuristics for combining and comparing induction schemas arc analysed as an example, how a rigorous formal approach may uncover implicit assumptions and hidden flaws. A containment test then is proposed as a powerful, non-heuristic, and completeness preserving operation to select among competing induction schemas. The motivation for this test evolves straightforwardly in the given-framework by recognizing the semantics of the intended effect

Authors

• Christoph Walther

Keywords

No keywords are indexed for this paper.