SMT-Solving Induction Proofs of Inequalities

TL;DR

This paper introduces a new dataset of non-linear real arithmetic problems for SMT solvers, based on an automated proof method for inequalities, and evaluates solver performance on these novel benchmarks.

Contribution

It presents a new dataset of inequality problems derived from Gerhold--Kauers' proof technique, expanding SMT benchmarking to previously unaddressed problem types.

Findings

Benchmarking reveals differences from existing datasets.

Highlights challenges with rational functions and algebraic numbers.

Provides a new proof example illustrating the technique.

Abstract

This paper accompanies a new dataset of non-linear real arithmetic problems for the SMT-LIB benchmark collection. The problems come from an automated proof procedure of Gerhold--Kauers, which is well suited for solution by SMT. The problems of this type have not been tackled by SMT-solvers before. We describe the proof technique and give one new such proof to illustrate it. We then describe the dataset and the results of benchmarking. The benchmarks on the new dataset are quite different to the existing ones. The benchmarking also brings forward some interesting debate on the use/inclusion of rational functions and algebraic numbers in the SMT-LIB.