Induction with Generalization in Superposition Reasoning

Hajdú, Márton; Hozzova, Petra; Kovacs, Laura; Schoisswohl, Johannes; Voronkov, Andrei

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

Record link:

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

Title:

Induction with Generalization in Superposition Reasoning

Citation:

Hajdú, M., Hozzova, P., Kovacs, 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

Publisher DOI:

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

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Authors:

Hajdú, Márton
Hozzova, Petra
Kovacs, Laura
Schoisswohl, Johannes
Voronkov, Andrei

Organisational Unit:

E192-04 - Forschungsbereich Formal Methods in Systems Engineering

Published in:

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

ISBN:

978-3-030-53517-9

Volume:

12236

DOI of the book:

10.1007/978-3-030-53518-6

Date (published):

26-Jul-2020

Number of Pages:

Publisher:

Springer, Cham

Peer reviewed:

Yes

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.

Project title:

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)

Project (external):

Engineering and Physical Sciences Research Council (EPSRC)
KAW Foundation

Project ID:

EP/P03408X/1
Wallenberg Academy fellowship 2014 TheProSE

License:

In Copyright

Appears in Collections:

Conference Paper