Title: Inductive Benchmarks for Automated Reasoning
Authors: Hajdu, Marton 
Hozzova, Petra 
Kovacs, Laura 
Schoisswohl, Johannes 
Voronkov, Andrei 
Issue Date: 12-Aug-2021
Citation: 
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 
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.
Keywords: automated reasoning; automated deduction; theorem proving
URI: http://hdl.handle.net/20.500.12708/18558
https://doi.org/10.34726/1563
DOI: 10.34726/1563
Organisation: E192-04 - Forschungsbereich Formal Methods in Systems Engineering 
License: In Copyright 1.0
Publication Type: Inproceedings
Konferenzbeitrag
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)

31
checked on May 7, 2022

Download(s)

21
checked on May 7, 2022

Google ScholarTM

Check