Download PDFOpen PDF in browser

Inductive Benchmarks for Automated Reasoning

EasyChair Preprint 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: Inductive data types, automated reasoning, inductive benchmarks, 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 5531},
  year      = {EasyChair, 2021}}
Download PDFOpen PDF in browser