This paper enriches a pre-existing decision algorithm, which in turn augmented a fragment of Tarski's elementary algebra with one-argument real functions endowed with a continuous first derivative. In its present (still quantifier-free) version, our decidable language embodies the addition of functions and multiplication of functions by scalars; 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 variables of another sort, out of which compound terms are formed by means of constructs designating addition and differentiation. An array of predicates designates 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-valued term. Our decision method consists in preprocessing the given formula into an equi-satisfiable 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 flexible-enough family of interpolating functions that can accommodate a model for the source formula whenever the target formula turns out to be satisfiable. With respect to the 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 involving addition of differentiable real functions

Omodeo E.;
2023-01-01

Abstract

This paper enriches a pre-existing decision algorithm, which in turn augmented a fragment of Tarski's elementary algebra with one-argument real functions endowed with a continuous first derivative. In its present (still quantifier-free) version, our decidable language embodies the addition of functions and multiplication of functions by scalars; 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 variables of another sort, out of which compound terms are formed by means of constructs designating addition and differentiation. An array of predicates designates 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-valued term. Our decision method consists in preprocessing the given formula into an equi-satisfiable 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 flexible-enough family of interpolating functions that can accommodate a model for the source formula whenever the target formula turns out to be satisfiable. With respect to the 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.
2023
Pubblicato
https://www.sciencedirect.com/science/article/abs/pii/S0304397522006533
File in questo prodotto:
File Dimensione Formato  
1-s2.0-S0304397522006533-main.pdf

Accesso chiuso

Tipologia: Documento in Versione Editoriale
Licenza: Copyright Editore
Dimensione 643.29 kB
Formato Adobe PDF
643.29 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
1-s2.0-S0304397522006533-main-Post_print.pdf

embargo fino al 04/11/2024

Tipologia: Bozza finale post-referaggio (post-print)
Licenza: Creative commons
Dimensione 1.15 MB
Formato Adobe PDF
1.15 MB Adobe PDF   Visualizza/Apri   Richiedi una copia
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/3041158
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact