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 SizeFormat
Automated Induction by Reflection.pdf590.91 kBAdobe PDFThumbnail
 View/Open
Show full item record

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.