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.
Decision algorithms for fragments of real analysis. I. Continuous functions with strict convexity and concavity predicates
CANTONE, Domenico;CINCOTTI, Gianluca;GALLO, Giovanni
2006-01-01
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.File | Dimensione | Formato | |
---|---|---|---|
CantoneCincottiGallo-JSC-2006.pdf
accesso aperto
Tipologia:
Versione Editoriale (PDF)
Dimensione
509.53 kB
Formato
Adobe PDF
|
509.53 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.