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

TL;DR

This paper develops a decision procedure for a fragment of real analysis involving differentiable functions with (semi-)open intervals, extending satisfiability tests to handle function properties and derivatives.

Contribution

It introduces a method to reduce formulas about differentiable functions over (semi-)open intervals to quantifier-free algebraic formulas, enabling satisfiability checking via Tarski's decision method.

Findings

Extended decision procedures to (semi)-open intervals.

Reduced function properties to algebraic formulas.

Enabled satisfiability checking of complex real analysis fragments.

Abstract

This paper enriches preexisting satisfiability tests for unquantified languages, which in turn augment a fragment of Tarski's elementary algebra with unary real functions possessing a continuous first derivative. Two sorts of individual variables are available, one ranging over real numbers and the other one ranging over the functions of interest. Numerical terms are built from real variables through constructs designating the four basic arithmetic operations and through the function-application constructs $f(t)$ and $D[\,f\,](t)$, where $f$ stands for a function variable, $t$ for a numerical term, and $D[\,\sqdot\,]$ designates the differentiation operator. Comparison relators can be placed between numerical terms. An array of predicate symbols are also available, designating various relationships between functions, as well as function properties, that may hold over intervals of the real line; those are: (pointwise) function comparisons, strict and nonstrict monotonicity~/~convexity~/~concavity properties, comparisons between the derivative of a function and a real term--here, w.r.t.\ earlier research, they are extended to (semi)-open intervals. The decision method we propose consists in preprocessing the given formula into an equisatisfiable quantifier-free formula of the elementary algebra of real numbers, whose satisfiability can then be checked by means of Tarski's decision method. No direct reference to functions will appear in the target formula, each function variable having been superseded by a collection of stub real variables; hence, in order to prove that the proposed translation is satisfiability-preserving, we must figure out a sufficiently flexible family of interpolating $C^1$ functions that can accommodate a model for the source formula whenever the target formula turns out to be satisfiable.