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.
| Original language | English |
|---|---|
| Pages (from-to) | 10-24 |
| Number of pages | 15 |
| Journal | CEUR Workshop Proceedings |
| Volume | 3458 |
| Publication status | Published - 19 Aug 2022 |
| Event | 7th International Workshop on Satisfiability Checking and Symbolic Computation Square Workshop, SC-Square 2022 - Haifa, Israel Duration: 12 Aug 2022 → … |
Bibliographical note
Funding Information:All three authors are supported by the EPSRC DEWCAD Project (Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition): JHD and AU by grant number EP/T015713/1 and ME by grant number EP/T015748/1. AU also acknowledges partial support from FWF grant P-34501N.
Funding
All three authors are supported by the EPSRC DEWCAD Project (Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition): JHD and AU by grant number EP/T015713/1 and ME by grant number EP/T015748/1. AU also acknowledges partial support from FWF grant P-34501N.
Keywords
- Computer Algebra
- Induction Proofs
- Inequalities
- Rational Functions
- Satisfiability Modulo Theories
ASJC Scopus subject areas
- General Computer Science