Decision algorithms for fragments of real analysis. I. Continuous functions with strict convexity and concavity predicates |
| |
Affiliation: | Department of Mathematics and Computer Science, University of Catania, Viale Andrea Doria 6, 95125 Catania, Italy |
| |
Abstract: | In this paper we address the decision problem for a fragment of unquantified formulae of real analysis, which, besides the operators of Tarski’s theory of reals, includes also strict and non-strict predicates expressing comparison, monotonicity, concavity, and convexity of continuous real functions over possibly unbounded intervals.The decision result is obtained by proving that a formula of our fragment is satisfiable if and only if it admits a parametric “canonical” model, whose existence can be tested by solving a suitable unquantified formula, expressed in the decidable language of Tarski’s theory of reals and involving the numerical variables of the initial formula plus various other parameters.This paper generalizes a previous decidability result concerning a more restrictive fragment in which predicates relative to infinite intervals or stating strict concavity and convexity were not expressible. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|