Eugenio G. Omodeo

TCS Journal 2023 Journal Article

A decidable theory involving addition of differentiable real functions

• Gabriele Buriola
• Domenico Cantone
• Gianluca Cincotti
• Eugenio G. Omodeo
• Gaetano T. Spartà

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 C 1 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.

TCS Journal 2023 Journal Article

Complexity assessments for decidable fragments of Set Theory. III: Testers for crucial, polynomial-maximal decidable Boolean languages

• Domenico Cantone
• Pietro Maugeri
• Eugenio G. Omodeo

We continue our investigation aimed at spotting small fragments of Set Theory (in this paper, sublanguages of Boolean Set Theory) that might be of use in automated proof-checkers based on the set-theoretic formalism. Here we propose a method that leads to a cubic-time satisfiability decision test for the language involving, besides variables intended to range over the von Neumann set-universe, the Boolean operator ∪ and the logical relators = and ≠. It can be seen that the dual language involving the Boolean operator ∩ and, again, the relators = and ≠, also admits a cubic-time satisfiability decision test; noticeably, the same algorithm can be used for both languages. Suitable pre-processing can reduce richer Boolean languages to the said two fragments, so that the same cubic satisfiability test can be used to treat the relators ⊆ and ⊈, and the predicates ‘ Image 1 ’ and ‘ Image 2 ’, meaning ‘the argument is empty’ and ‘the arguments are disjoint sets’, along with their opposites ‘ Image 3 ’ and ‘ Image 4 ’. Those richer languages are ‘polynomial maximal’, in the sense that each language strictly containing either of them and whose formulae are conjunctions of literals has an NP-hard satisfiability problem. A generalized version of the two said satisfiability tests can treat the relator ⊄, though at the price of a worsening of the algorithmic complexity (from cubic to quintic time).

TCS Journal 2020 Journal Article

Complexity assessments for decidable fragments of set theory. II: A taxonomy for ‘small’ languages involving membership

• Domenico Cantone
• Pietro Maugeri
• Eugenio G. Omodeo

We carry on a long-standing investigation aimed at identifying fragments of set theory that are potentially useful in automated verification with proof-checkers, such as ÆtnaNova, based on the set-theoretic formalism. This note provides a complete taxonomy of the polynomial and the NP-complete fragments consisting of all conjunctions that involve, besides variables intended to range over the von Neumann set-universe, a collection of constructs drawn from the Boolean set operators ∪, ∩, ∖ and the membership relators ∈ and ∉. This is done in sight of combining the aforementioned taxonomy with one recently put together for analogous fragments involving, in place of the relators ∈ and ∉, the Boolean relators ⊆, = and the predicates ‘ ⋅ = ∅ ’ and ‘ Disj ( ⋅, ⋅ ) ’ (respectively meaning ‘the argument set is empty’ and ‘the arguments are disjoint sets’), along with their opposites ‘ ⊈, ≠, ⋅ ≠ ∅ ’ and ‘ ¬ Disj ( ⋅, ⋅ ) ’.

TCS Journal 2004 Journal Article

ER modelling from first relational principles

• Ernst-Erich Doberkat
• Eugenio G. Omodeo

Entity-Relationship (ER) modelling is a popular technique for data modelling. Despite its popularity and widespread use, it lacks a firm semantic foundation. We propose a translation of an ER-model into relation algebra, suggesting that this kind of algebra does provide suitable mechanisms for establishing a formal semantics of ER modelling. The work reported on here deals first with the techniques necessary for the translation, thus constructing a static view of an ER-model in an abstract setting of what might be called logic without variables. We then undertake a detailed analysis of the insertion and deletion operations for an ER-model represented in terms of the relation calculus.

I&C Journal 2002 Journal Article

Formative Processes with Applications to the Decision Problem in Set Theory

• Domenico Cantone
• Pietro Ursino
• Eugenio G. Omodeo

This paper introduces formative processes, composed by transitive partitions. Given a family F of sets, a formative process ending in the Venn partition Σ of F is shown to exist. Sufficient criteria are also singled out for a transitive partition to model (via a function from set variables to unions of sets in the partition) all set-literals modeled by Σ. On the basis of such criteria a procedure is designed that mimics a given formative process by another where sets have finite rank bounded by C(|Σ|), with C a specific computable function. As a by-product, one of the core results on decidability in computable set theory is rediscovered, namely the one that regards the satisfiability of unquantified set-theoretic formulae involving Boolean operators, the singleton-former, and the powerset operator. The method described (which is able to exhibit a set-solution when the answer is affirmative) can be extended to solve the satisfiability problem for broader fragments of set theory.

ECAI Conference 1990 Conference Paper

Truth Tables for a Combinatorial Kernel of Set Theories

• Eugenio G. Omodeo
• Franco Parlamento
• Alberto Policriti

IJCAI Conference 1989 Conference Paper

On the Decidability of Formulae Involving Continuous and Closed Functions

• Domenico Cantone
• Eugenio G. Omodeo