Automating Induction by Reflection
| Autor: | Schoisswohl, Johannes, Kovács, Laura |
|---|---|
| Rok vydání: | 2021 |
| Předmět: | |
| Zdroj: | EPTCS 337, 2021, pp. 39-54 |
| Druh dokumentu: | Working Paper |
| DOI: | 10.4204/EPTCS.337.4 |
| Popis: | 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. Comment: In Proceedings LFMTP 2021, arXiv:2107.07376. A full version of this paper appears at arXiv:2106.05066 |
| Databáze: | arXiv |
| Externí odkaz: |
|