Title: Inductive Benchmarks for Automated Reasoning
Authors: Hajdu, Marton 
Hozzova, Petra 
Kovacs, Laura 
Schoisswohl, Johannes 
Voronkov, Andrei 
Issue Date: 12-Aug-2021
Hajdu, M., Hozzova, P., Kovacs, L., Schoisswohl, J., & Voronkov, A. (2021). Inductive Benchmarks for Automated Reasoning. In Proceedings of CICM 2021 (pp. 124–129). Springer, Cham. https://doi.org/10.34726/1563
Book Title: Proceedings of CICM 2021 
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.
Keywords: automated reasoning; automated deduction; theorem proving
URI: http://hdl.handle.net/20.500.12708/18558
DOI: 10.34726/1563
Organisation: E192-04 - Forschungsbereich Formal Methods in Systems Engineering 
License: In Copyright 1.0
Publication Type: Inproceedings
Appears in Collections:Conference Paper

Files in this item:

Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.

Page view(s)

checked on May 7, 2022


checked on May 7, 2022

Google ScholarTM