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:


Page view(s)

21
checked on Nov 25, 2021

Download(s)

13
checked on Nov 25, 2021

Google ScholarTM

Check


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