@inproceedings{460ea3de53394016bc6541e3594d809f,
title = "SMT-Solving Induction Proofs of Inequalities",
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.",
keywords = "Inequalities, Induction Proofs, Satisfiability Modulo Theories, Computer Algebra, Rational Functions",
author = "Ali Uncu and Davenport, {James H.} and Matthew England",
note = "Copyright {\textcopyright} 2023 for the individual papers by the papers' authors. Copyright {\textcopyright} 2023 for the volume as a collection by its editors. This volume and its papers are published under the Creative Commons License Attribution 4.0 International (CC BY 4.0). ; SC2 Workshop 2022 : Satisfiability Checking and Symbolic Computation ; Conference date: 12-08-2022 Through 12-08-2022",
year = "2023",
month = aug,
day = "18",
language = "English",
volume = "3458",
series = "CEUR Workshop Proceedings",
publisher = "CEUR Workshop Proceedings",
pages = "10--24",
editor = "Ali Uncu and Haniel Barbosa",
booktitle = "Proceedings of the 7th International Workshop on Satisfiability Checking and Symbolic Computation",
address = "Germany",
url = "http://www.sc-square.org/CSA/workshop7.html",
}
