Title: Automated induction by reflection
Language: English
Authors: Schoisswohl, Johannes 
Qualification level: Diploma
Advisor: Kovacs, Laura 
Issue Date: 2020
Number of Pages: 57
Qualification level: Diploma
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.
Keywords: automated reasoning; first-order theorem proving; mathematical induction
URI: https://doi.org/10.34726/hss.2020.75342
DOI: 10.34726/hss.2020.75342
Library ID: AC16108258
Organisation: E192 - Institut für Logic and Computation 
Publication Type: Thesis
Appears in Collections:Thesis

Files in this item:

Show full item record

Page view(s)

checked on Jun 3, 2021


checked on Jun 3, 2021

Google ScholarTM


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