-
Decision algorithms for fragments of real analysis. III: A theory of differentiable functions with (semi-)open intervals
Authors:
G. Buriola,
D. Cantone,
G. Cincotti,
E. G. Omodeo,
G. T. SpartÃ
Abstract:
This paper enriches preexisting satisfiability tests for unquantified languages, which in turn augment a fragment of Tarski's elementary algebra with unary real functions possessing a continuous first derivative.
Two sorts of individual variables are available, one ranging over real numbers and the other one ranging over the functions of interest. Numerical terms are built from real variables th…
▽ More
This paper enriches preexisting satisfiability tests for unquantified languages, which in turn augment a fragment of Tarski's elementary algebra with unary real functions possessing a continuous first derivative.
Two sorts of individual variables are available, one ranging over real numbers and the other one ranging over the functions of interest. Numerical terms are built from real variables through constructs designating the four basic arithmetic operations and through the function-application constructs $f(t)$ and $D[\,f\,](t)$, where $f$ stands for a function variable, $t$ for a numerical term, and $D[\,\sqdot\,]$ designates the differentiation operator. Comparison relators can be placed between numerical terms. An array of predicate symbols are also available, designating various relationships between functions, as well as function properties, that may hold over intervals of the real line; those are: (pointwise) function comparisons, strict and nonstrict monotonicity~/~convexity~/~concavity properties, comparisons between the derivative of a function and a real term--here, w.r.t.\ earlier research, they are extended to (semi)-open intervals.
The decision method we propose consists in preprocessing the given formula into an equisatisfiable 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 sufficiently flexible family of interpolating $C^1$ functions that can accommodate a model for the source formula whenever the target formula turns out to be satisfiable.
△ Less
Submitted 3 July, 2025;
originally announced July 2025.
-
Martin Davis: An Overview of his Work in Logic, Computer Science, and Philosophy
Authors:
Liesbeth De Mol,
Yuri V. Matiyasevich,
Eugenio G. Omodeo,
Alberto Policriti,
Wilfried Sieg,
Elaine J. Weyuker
Abstract:
In his autobiographic essay written in 1999, ``From logic to computer science and back'', Martin David Davis (3/8/1928--1/1/2023) indicated that he viewed himself as a logician \emph{and} a computer scientist. He expanded the essay in 2016 and expressed a new perspective through a changed title, ``My life as a logician''. He points out that logic was the unifying theme underlying his scientific ca…
▽ More
In his autobiographic essay written in 1999, ``From logic to computer science and back'', Martin David Davis (3/8/1928--1/1/2023) indicated that he viewed himself as a logician \emph{and} a computer scientist. He expanded the essay in 2016 and expressed a new perspective through a changed title, ``My life as a logician''. He points out that logic was the unifying theme underlying his scientific career. Our paper attempts to provide a consistent vision that illuminates Davis' successive contributions leading to his landmark writings on computability, unsolvable problems, automated reasoning, as well as the history and philosophy of computing.
△ Less
Submitted 10 June, 2025;
originally announced June 2025.
-
In Memory of Martin Davis
Authors:
Wesley Calvert,
Valentina Harizanov,
Eugenio G. Omodeo,
Alberto Policriti,
Alexandra Shlapentokh
Abstract:
The present paper gives an account for the general mathematical reader of the life and work of Martin Davis. Since two rather comprehensive autobiographical accounts and two long biographical interviews already exist, the present work focusses on Davis's scientific achievements, including work on computably enumerable sets, universal Turing machines, the hyperarithmetical hierarchy, neural network…
▽ More
The present paper gives an account for the general mathematical reader of the life and work of Martin Davis. Since two rather comprehensive autobiographical accounts and two long biographical interviews already exist, the present work focusses on Davis's scientific achievements, including work on computably enumerable sets, universal Turing machines, the hyperarithmetical hierarchy, neural networks, Hilbert's Tenth Problem, and automated reasoning.
△ Less
Submitted 15 January, 2024;
originally announced January 2024.
-
Complexity assessments for decidable fragments of Set Theory. IV: A quadratic reduction of constraints over nested sets to Boolean formulae
Authors:
Domenico Cantone,
Andrea De Domenico,
Pietro Maugeri,
Eugenio G. Omodeo
Abstract:
As a contribution to quantitative set-theoretic inferencing, a translation is proposed of conjunctions of literals of the forms $x=y\setminus z$, $x \neq y\setminus z$, and $z =\{x\}$, where $x,y,z$ stand for variables ranging over the von Neumann universe of sets, into unquantified Boolean formulae of a rather simple conjunctive normal form. The formulae in the target language involve variables r…
▽ More
As a contribution to quantitative set-theoretic inferencing, a translation is proposed of conjunctions of literals of the forms $x=y\setminus z$, $x \neq y\setminus z$, and $z =\{x\}$, where $x,y,z$ stand for variables ranging over the von Neumann universe of sets, into unquantified Boolean formulae of a rather simple conjunctive normal form. The formulae in the target language involve variables ranging over a Boolean ring of sets, along with a difference operator and relators designating equality, non-disjointness and inclusion. Moreover, the result of each translation is a conjunction of literals of the forms $x=y\setminus z$, $x\neq y\setminus z$ and of implications whose antecedents are isolated literals and whose consequents are either inclusions (strict or non-strict) between variables, or equalities between variables. Besides reflecting a simple and natural semantics, which ensures satisfiability-preservation, the proposed translation has quadratic algorithmic time-complexity, and bridges two languages both of which are known to have an NP-complete satisfiability problem.
△ Less
Submitted 12 November, 2022; v1 submitted 9 December, 2021;
originally announced December 2021.
