Inductive Benchmarks for Automated Reasoning

EasyChair Preprint 5531

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

@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}}