Induction with Generalization in Superposition Reasoning

Hajdú, Márton; Hozzová, Petra; Kovács, Laura; Schoisswohl, Johannes; Voronkov, Andrei

doi:10.1007/978-3-030-53518-6_8

Datensatz Zitierlink:

http://hdl.handle.net/20.500.12708/16998
https://doi.org/10.34726/961

Titel:

Induction with Generalization in Superposition Reasoning

Zitat:

Hajdú, M., Hozzová, P., Kovács, L., Schoisswohl, J., & Voronkov, A. (2020). Induction with Generalization in Superposition Reasoning. In Proceedings of the 13th International Conference on Intelligent Computer Mathematics (CICM) (pp. 123–137). Springer. https://doi.org/10.34726/961

reposiTUm-DOI:

10.34726/961

CatalogPlus:

AC17203908

Verlags-DOI:

10.1007/978-3-030-53518-6_8

Publikationstyp:

Konferenzbeitrag - Full-Paper Contribution

Sprache:

Englisch

Autor_innen:

Hajdú, Márton
Hozzová, Petra
Kovács, Laura
Schoisswohl, Johannes
Voronkov, Andrei

Organisationseinheit:

E192-04 - Forschungsbereich Formal Methods in Systems Engineering

Erschienen in:

Proceedings of the 13th International Conference on Intelligent Computer Mathematics (CICM)

ISBN:

978-3-030-53517-9

Band:

12236

DOI des Buches:

10.1007/978-3-030-53518-6

Datum (veröffentlicht):

26-Jul-2020

Umfang:

Verlag:

Springer, Cham

Peer Reviewed:

Keywords:

automated reasoning; induction; first-order theorem proving

Abstract:

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.

Projekttitel:

Symbolic Computation and Automated Reasoning for Program Analysis: 639270 (European Research Council (ERC))
Symbol Elimination in Reliable System Engineering: 842066 (European Commission)
Doktoratskolleg: W1255-N23 (Austrian Science Fund (FWF))
Domänenspezifisches Schließen in IoT Anwendungen (Vereine, Stiftungen, Preise)

Projekt (extern):

Engineering and Physical Sciences Research Council (EPSRC)
KAW Foundation

Projektnummer:

EP/P03408X/1
Wallenberg Academy fellowship 2014 TheProSE

Lizenz:

Urheberrechtsschutz

Enthalten in den Sammlungen:

Conference Paper