<div class="csl-bib-body">
<div class="csl-entry">Hozzová, P., Kovács, L., & Voronkov, A. (2021). Integer Induction in Saturation. In <i>Proceedings of CADE 2021</i> (pp. 361–377). Springer, Cham. https://doi.org/10.34726/1561</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/18556
-
dc.identifier.uri
https://doi.org/10.34726/1561
-
dc.description.abstract
Integers are ubiquitous in programming and therefore also in applications of program analysis and verification. Such applications often require some sort of inductive reasoning. In this paper we analyze the challenge of automating inductive reasoning with integers. We introduce inference rules for integer induction within the saturation framework of first-order theorem proving. We implemented these rules in the theorem prover Vampire and evaluated our work against other state-of-the-art theorem provers. Our results demonstrate the strength of our approach by solving new problems coming from program analysis and mathematical properties of integers.
en
dc.description.sponsorship
European Commission
-
dc.description.sponsorship
European Commission
-
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture notes in computer science
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
automated reasoning
en
dc.subject
theorem proving
en
dc.subject
automated deduction
en
dc.title
Integer Induction in Saturation
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Urheberrechtsschutz
de
dc.rights.license
In Copyright
en
dc.identifier.doi
10.34726/1561
-
dc.contributor.affiliation
University of Manchester, United Kingdom of Great Britain and Northern Ireland (the)
