Automating Induction by Reflection

TL;DR

This paper introduces a novel method for formalizing schematic inductive definitions within standard first-order logic, enabling automated inductive reasoning with theorem provers, and compares its practical effectiveness to existing techniques.

Contribution

The paper presents a new approach inspired by axiomatic theories of truth to express schematic inductive definitions in first-order logic, facilitating automation.

Findings

Method successfully formalizes schematic inductive definitions in first-order logic.

Compared to native techniques, the method shows promising results in theorem proving tasks.

Practical feasibility demonstrated with state-of-the-art theorem provers.

Abstract

Despite recent advances in automating theorem proving in full first-order theories, inductive reasoning still poses a serious challenge to state-of-the-art theorem provers. The reason for that is that in first-order logic induction requires an infinite number of axioms, which is not a feasible input to a computer-aided theorem prover requiring a finite input. Mathematical practice is to specify these infinite sets of axioms as axiom schemes. Unfortunately these schematic definitions cannot be formalized in first-order logic, and therefore not supported as inputs for first-order theorem provers. In this work we introduce a new method, inspired by the field of axiomatic theories of truth, that allows to express schematic inductive definitions, in the standard syntax of multi-sorted first-order logic. Further we test the practical feasibility of the method with state-of-the-art theorem provers, comparing it to solvers' native techniques for handling induction. This paper is an extended version of the LFMTP 21 submission with the same title.