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.
Titolo: | Decision algorithms for fragments of real analysis. I. Continuous functions with strict convexity and concavity predicates |
Autori interni: | |
Data di pubblicazione: | 2006 |
Rivista: | |
Citazione: | Decision algorithms for fragments of real analysis. I. Continuous functions with strict convexity and concavity predicates / CANTONE D; CINCOTTI G; GALLO G. - In: JOURNAL OF SYMBOLIC COMPUTATION. - ISSN 0747-7171. - 41:7(2006), pp. 763-789. |
Handle: | http://hdl.handle.net/20.500.11769/25002 |
Appare nelle tipologie: | 1.1 Articolo in rivista |