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.
