Title: | Automated Induction by Reflection | Other Titles: | Automated Induction by Reflection | Language: | English | Authors: | Schoisswohl, Johannes | Qualification level: | Diploma | Keywords: | automated reasoning; first-order theorem proving; mathematical induction | Advisor: | Kovacs, Laura | Issue Date: | 2020 | Number of Pages: | 57 | Qualification level: | Diploma | Abstract: | Despite the advances in automated theorem proving in the last decades, making it practically feasible to reason about full first-order logic with interpreted equality and more, 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 feasible as an input for a theorem prover that is a computer program, requiring a finite input. Mathematical practice is to specify these infinite sets of axioms as axiom schemes. Unfortunately these schematic definitions are not part of the syntax of first-order logic, and therefore not supported as an input for modern theorem provers.In this thesis we introduce a new method, inspired by the field of axiomatic theories of truth, that allows to the express schematic definitions needed for first-order induction, in the standard syntax of multi-sorted first-order logic. Further the practical feasibility of this method is tested with state-of-the-art theorem provers, by comparing it to solvers native techniques for handling induction. |
URI: | https://doi.org/10.34726/hss.2020.75342 http://hdl.handle.net/20.500.12708/16472 |
DOI: | 10.34726/hss.2020.75342 | Library ID: | AC16108258 | Organisation: | E192 - Institut für Logic and Computation | Publication Type: | Thesis Hochschulschrift |
Appears in Collections: | Thesis |
Files in this item:
File | Description | Size | Format | |
---|---|---|---|---|
Automated Induction by Reflection.pdf | 590.91 kB | Adobe PDF | ![]() View/Open |
Page view(s)
23
checked on Feb 27, 2021
Download(s)
42
checked on Feb 27, 2021

Google ScholarTM
Check
Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.