Inductive Benchmarks for Automated Reasoning
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.
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
8
References
0
Citations
NaN
KQI