Download PDFOpen PDF in browser

Inductive Benchmarks for Automated Reasoning

EasyChair Preprint no. 5531

5 pagesDate: May 17, 2021

Abstract

In this paper we present a 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.

Keyphrases: automated reasoning, inductive benchmarks, Inductive data types, integers

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@Booklet{EasyChair:5531,
  author = {Márton Hajdu and Petra Hozzová and Laura Kovács and Johannes Schoisswohl and Andrei Voronkov},
  title = {Inductive Benchmarks for Automated Reasoning},
  howpublished = {EasyChair Preprint no. 5531},

  year = {EasyChair, 2021}}
Download PDFOpen PDF in browser