Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2412.16091 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911004102754304 |
|---|---|
| author | Cantone, Domenico Cincotti, Gianluca |
| author_facet | Cantone, Domenico Cincotti, Gianluca |
| contents | We address the decision problem for a fragment of real analysis involving differentiable functions with continuous first derivatives. The proposed theory, besides the operators of Tarski's theory of reals, includes predicates for comparisons, monotonicity, convexity, and derivative of functions over bounded closed intervals or unbounded intervals.
Our decision algorithm is obtained by showing that satisfiable formulae of our theory admit canonical models in which functional variables are interpreted as piecewise exponential functions. These can be implicitly described within the decidable Tarski's theory of reals.
Our satisfiability test generalizes previous decidability results not involving derivative operators. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2412_16091 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Decision algorithms for fragments of real analysis. II. A theory of differentiable functions with convexity and concavity predicates Cantone, Domenico Cincotti, Gianluca Logic in Computer Science 03B25, 26A99 We address the decision problem for a fragment of real analysis involving differentiable functions with continuous first derivatives. The proposed theory, besides the operators of Tarski's theory of reals, includes predicates for comparisons, monotonicity, convexity, and derivative of functions over bounded closed intervals or unbounded intervals. Our decision algorithm is obtained by showing that satisfiable formulae of our theory admit canonical models in which functional variables are interpreted as piecewise exponential functions. These can be implicitly described within the decidable Tarski's theory of reals. Our satisfiability test generalizes previous decidability results not involving derivative operators. |
| title | Decision algorithms for fragments of real analysis. II. A theory of differentiable functions with convexity and concavity predicates |
| topic | Logic in Computer Science 03B25, 26A99 |
| url | https://arxiv.org/abs/2412.16091 |