<div class="csl-bib-body">
<div class="csl-entry">Kovács, L., Hozzová, P., Hajdu, M., & Voronkov, A. (2024). Induction in Saturation. In <i>Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I</i> (pp. 21–29). Springer. https://doi.org/10.1007/978-3-031-63498-7_2</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/199514
-
dc.description.abstract
Proof by induction is commonplace in modern mathematics and computational logic. This paper overviews and discusses our recent results in turning saturation-based first-order theorem proving into a powerful framework for automating inductive reasoning. We formalize applications of induction as new inference rules of the saturation process, add instances of appropriate induction schemata to the search space, and use these rules and instances immediately upon their addition for the purpose of guiding induction. Our results show, for example, that many problems from formal verification and mathematical theories can now be solved completely automatically using a first-order theorem prover.
en
dc.description.sponsorship
European Commission
-
dc.description.sponsorship
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
-
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.language.iso
en
-
dc.relation.ispartofseries
LNCS
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
induction
en
dc.subject
automated reasoning
en
dc.subject
first-order theorem proving
en
dc.title
Induction in Saturation
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.contributor.affiliation
University of Manchester, United Kingdom of Great Britain and Northern Ireland (the)
