This paper enriches a pre-existing decision algorithm, which in its turn augmented a fragment of Tarski’s elementary algebra with one-argument real functions endowed with continuous first derivative. In its present (still quantifier-free) version, our decidable language embodies addition of functions; the issue we address is the one of satisfiability. As regards real numbers, individual variables and constructs designating the basic arithmetic operations are available, along with comparison relators. As regards functions, we have another sort of variables, out of which compound terms are formed by means of constructs designating addition and—outermostly—differentiation. An array of predicates designate various relationships between functions, as well as function properties, that may hold over intervals of the real line; those are: function comparisons, strict and non-strict monotonicity / convexity / concavity, comparisons between the derivative of a function and a real term. With respect to results announced in earlier papers of the same stream, a significant effort went into designing the family of interpolating functions so that it could meet the new constraints stemming from the presence of function addition (along with differentiation) among the constructs of our fragment of mathematical analysis.

A Decidable Theory Treating Addition of Differentiable Real Functions.

Eugenio Omodeo;
2021-01-01

Abstract

This paper enriches a pre-existing decision algorithm, which in its turn augmented a fragment of Tarski’s elementary algebra with one-argument real functions endowed with continuous first derivative. In its present (still quantifier-free) version, our decidable language embodies addition of functions; the issue we address is the one of satisfiability. As regards real numbers, individual variables and constructs designating the basic arithmetic operations are available, along with comparison relators. As regards functions, we have another sort of variables, out of which compound terms are formed by means of constructs designating addition and—outermostly—differentiation. An array of predicates designate various relationships between functions, as well as function properties, that may hold over intervals of the real line; those are: function comparisons, strict and non-strict monotonicity / convexity / concavity, comparisons between the derivative of a function and a real term. With respect to results announced in earlier papers of the same stream, a significant effort went into designing the family of interpolating functions so that it could meet the new constraints stemming from the presence of function addition (along with differentiation) among the constructs of our fragment of mathematical analysis.
File in questo prodotto:
File Dimensione Formato  
paper13.pdf

accesso aperto

Descrizione: Articolo principale
Tipologia: Documento in Versione Editoriale
Licenza: Creative commons
Dimensione 609.8 kB
Formato Adobe PDF
609.8 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11368/3005853
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact