Decision algorithms for fragments of real analysis. II. A theory of differentiable functions with convexity and concavity predicates

2024/12/20 by Domenico Cantone, Cantone, Domenico, Gianluca Cincotti +1 · 1 citation
Computer Science · #03B25 #26A99 #Advanced Computational Techniques in Science and Engineering #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · pdf · doi:10.48550/arxiv.2412.16091

openalex publication_date 2024/12/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

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.

Cited by

• Decision algorithms for fragments of real analysis. III: A theory of differentiable functions with (semi-)open intervals

Related

• Decision algorithms for fragments of real analysis. III: A theory of differentiable functions with (semi-)open intervals
• Deciding Predicate Logical Theories of Real-Valued Functions
• The generic differentiability of convex-concave functions: Characterization
• Would Real Analysis be complete without the Fundamental Theorem of Calculus?
• On the piecewise-concave approximations of functions