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

TL;DR

This paper develops a decision algorithm for a fragment of real analysis involving differentiable functions with convexity and concavity predicates, extending previous results to include derivatives.

Contribution

It introduces a new decidable theory for differentiable functions with convexity and concavity, using canonical models with piecewise exponential functions.

Findings

Decidable theory for differentiable functions with convexity and concavity predicates.

Satisfiable formulas have canonical models interpretable as piecewise exponential functions.

Generalizes previous decidability results to include derivative operators.

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.