Combining Induction Axioms by Machine

Abstract

The combination of induction axioms is investigated. It is shown how a pair of competing induction axioms (which e.g. are suggested by a heuristic of an induction theorem prover on a specific verification problem) are combined yielding a new induction axiom. The relation implicitly defined by the new axiom is the set-theoretic union of the well-founded relations implicitly defined by the induction axioms initially given. The proposed approach is non-heuristic but safe in the sense that an induction proof with the new axiom can be obtained whenever an induction proof with one of the given axioms would have been successful. Based on a result of Bachmair and Dershowitz for proving term rewriting systems noetherian, a commutation test is developed as a deductive requirement to verify the soundness of the combined axiom: It is shown how so-called commutation formulas can be derived by machine from the given axioms such that a verification of these formulas (e.g. by an induction theorem prover) guarantees the well-foundedness of the relation defined by the combined axiom. Examples are presented to demonstrate the usefulness and strength of the proposed technique.