Inductive Benchmarks for Automated Reasoning

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

doi:10.1007/978-3-030-81097-9_9

Record link:

http://hdl.handle.net/20.500.12708/18558
https://doi.org/10.34726/1563

Title:

Inductive Benchmarks for Automated Reasoning

Citation:

Hajdu, M., Hozzová, P., Kovács, L., Schoisswohl, J., & Voronkov, A. (2021). Inductive Benchmarks for Automated Reasoning. In Intelligent Computer Mathematics. 14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings (pp. 124–129). Springer. https://doi.org/10.34726/1563

reposiTUm DOI:

10.34726/1563

CatalogPlus:

AC17204390

Publisher DOI:

10.1007/978-3-030-81097-9_9

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Authors:

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

Organisational Unit:

E192-04 - Forschungsbereich Formal Methods in Systems Engineering

Published in:

Intelligent Computer Mathematics. 14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings

ISBN:

978-3-030-81097-9

Volume:

12833

DOI of the book:

10.1007/978-3-030-81097-9

Date (published):

12-Aug-2021

Number of Pages:

Publisher:

Springer, Cham

Peer reviewed:

Yes

Keywords:

automated reasoning; automated deduction; theorem proving

Abstract:

We present a large set of benchmarks for automated theorem provers that require inductive reasoning. Motivated by the need to compare first-order theorem provers, SMT solvers and inductive theorem provers, the setting of our examples follows the SMT-LIB standard. Our benchmark set contains problems with inductive data types as well as integers. In addition to SMT-LIB encodings, we provide translations to some other less common input formats.

Project title:

Symbolic Computation and Automated Reasoning for Program Analysis: 639270 (European Commission)
Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission)

License:

In Copyright

Appears in Collections:

Conference Paper