The Vampire Approach to Induction (short paper)

Hajdu, Márton; Kovács, Laura; Rawson, Michael; Voronkov, Andrei

doi:10.34726/4103

Record link:

http://hdl.handle.net/20.500.12708/177096
https://doi.org/10.34726/4103

Title:

The Vampire Approach to Induction (short paper)

Citation:

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.), PAAR 2022. Practical Aspects of Automated Reasoning 2022. Proceedings of the Workshop on Practical Aspects of Automated Reasoning. https://doi.org/10.34726/4103

reposiTUm DOI:

10.34726/4103

CatalogPlus:

AC17204664

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Authors:

Hajdu, Márton
Kovács, Laura
Rawson, Michael
Voronkov, Andrei

Organisational Unit:

E192-04 - Forschungsbereich Formal Methods in Systems Engineering

Published in:

PAAR 2022. Practical Aspects of Automated Reasoning 2022. Proceedings of the Workshop on Practical Aspects of Automated Reasoning

Volume:

3201

Date (published):

31-Aug-2022

Event name:

Practical Aspect of Automated Reasoning

Event date:

11-Aug-2022 - 12-Aug-2022

Event place:

Haifa, Israel

Number of Pages:

Peer reviewed:

Yes

Keywords:

inductive reasoning; saturation-based theorem proving; Superposition Calculus; First-order theorem proving

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.

Project (external):

ERC CoG ARTIST
EPSRC
Austrian Science Fund (FWF

Project ID:

101002685
P03408X
W1255-N23

Link (external):

https://nbn-resolving.org/urn:nbn:de:0074-3201-6

Research Areas:

Mathematical and Algorithmic Foundations: 50%
Computer Science Foundations: 50%

Science Branch:

1020 - Informatik: 80%
1010 - Mathematik: 20%

License:

CC BY 4.0