Title: Induction with Generalization in Superposition Reasoning
Authors: Hajdú, Márton 
Hozzova, Petra 
Kovacs, Laura 
Schoisswohl, Johannes 
Voronkov, Andrei  
Issue Date: 26-Jul-2020
Book Title: Proceedings of the 13th International Conference on Intelligent Computer Mathematics (CICM) 
We describe an extension of automating induction in superposition-based reasoning by strengthening inductive properties and generalizing terms over which induction should be applied. We implemented our approach in the first-order theorem prover Vampire and evaluated our work against state-of-the-art reasoners automating induction. We demonstrate the strength of our technique by showing that many interesting mathematical properties of natural numbers and lists can be proved automatically using this extension.
Keywords: automated reasoning; induction; first-order theorem proving
URI: http://hdl.handle.net/20.500.12708/16998
DOI: 10.34726/961
Organisation: E192-04 - Forschungsbereich Formal Methods in Systems Engineering 
License: Urheberrechtsschutz 1.0
Publication Type: Inproceedings
Appears in Collections:Conference Paper

Files in this item:

File Description SizeFormat
Hajdu - 2020 - Induction with generalization in superposition reasoning.pdfPostprint was published at CICM 2020.300.29 kBAdobe PDFThumbnail
Show full item record

Page view(s)

checked on Jun 6, 2021


checked on Jun 6, 2021

Google ScholarTM


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