<div class="csl-bib-body">
<div class="csl-entry">Hajdu, M., Kovács, L., Rawson, M., & Voronkov, A. (2022). The Vampire Approach to Induction (short paper). In B. Konev, C. Schon, & A. Steen (Eds.), <i>PAAR 2022. Practical Aspects of Automated Reasoning 2022. Proceedings of the Workshop on Practical Aspects of Automated Reasoning</i>. https://doi.org/10.34726/4103</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/177096
-
dc.identifier.uri
https://doi.org/10.34726/4103
-
dc.description.abstract
We discuss practical aspects of automating inductive reasoning in the first-order superposition prover Vampire. We explore solutions for reasoning over inductively defined dataypes; generating, storing and applying induction schema instances; and directly integrating inductive reasoning into the saturation reasoning loop of Vampire. Our techniques significantly improve the performance of Vampire despite the inherent difficulty of automated induction. We expect our exposition to be useful when implementing induction in saturation-style provers, and to stimulate further discussion and advances in the area.
en
dc.language.iso
en
-
dc.relation.ispartofseries
(CEUR) Workshop Proceedings
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
inductive reasoning
en
dc.subject
saturation-based theorem proving
en
dc.subject
Superposition Calculus
en
dc.subject
First-order theorem proving
en
dc.title
The Vampire Approach to Induction (short paper)
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.identifier.doi
10.34726/4103
-
dc.contributor.affiliation
University of Manchester, United Kingdom of Great Britain and Northern Ireland (the)
-
dc.contributor.editoraffiliation
University of Liverpool, United Kingdom of Great Britain and Northern Ireland (the)
