Recent publications coauthored by Eugenio Omodeo

J.T. Schwartz
D. Cantone, and
E.G. Omodeo,
. SpringerVerlag, 2011.
 A.Formisano,
E.G.Omodeo,
E.S. Orłowska, and A. Policriti.
Uniform relational frameworks for modal inferences, in preparation.
Abstract
In this paper we discuss how equational reasoning in relation
algebras can be applied to modal logics. We recall the two kinds
of translation of modal languages into relational languages: a
translation which enables one to apply directly the relational
tools to reasoning in modal logics, and a theorybased
translation. We show how the intermediate theory employed in the
second kind of translation must be enhanced in order to allow for
equational relational reasoning.
Key words:
Modal logic,
relational systems, translation methods.

A.Dovier,
A.Formisano,
and
E.G.Omodeo.
Decidability Results for Sets with Atoms.
ACM Transactions on Computational Logic (TOCL), 7(2)269301, 2006.
Abstract
Formal Set Theory is traditionally concerned with
pure sets; consequently, the satisfiability problem for
fragments of set theory was most often addressed (and in many
cases positively solved) in the pure framework. In practical
applications, however, it is common to assume the existence of a
number of primitive objects (sometimes called atoms) that
can be members of sets but behave differently from them. If these
entities are assumed to be devoid of members, the standard
extensionality axiom must be revised; then decidability results
can sometimes be achieved via reduction to the pure case and
sometimes can be based on direct goaldriven algorithms. An
alternative approach to modeling atoms, that allows one to retain
the original formulation of extensionality, was proposed by Quine:
atoms are selfsingletons. In this paper we adopt this approach in
coping with the satisfiability problem: we show the decidability
of this problem relativized to $\exists^{\ast}\forall$sentences
and we develop a goaldriven unification algorithm.
Key words:
Sethyperset theories,
Satisfiability problem, Syllogistics, Prenex sentences,
Quantifier elimination, Unification.

A.Formisano,
E.G.Omodeo,
and
A.Policriti.
The axiom of elementary sets on the edge of Peircean expressibility.
Journal of Symbolic Logic, 70(3):953968, 2005.
Abstract
Being able to state the principles which lie deepest in the
foundations of mathematics by sentences in three variables is
crucially important for a satisfactory equational rendering of set
theories along the lines proposed by Alfred Tarski and Steven
Givant in their monograph of 1987.
The main achievement of this paper is the proof that the `kernel'
set theory whose postulates are \emph{extensionality},
(E), and singleelement adjunction and
removal, (W) and (L), cannot be
axiomatized by means of threevariable sentences. This highlights
a sharp edge to be crossed in order to attain an `algebraization'
of Set Theory. Indeed, one easily shows that the theory which
results from the said kernel by addition of the null set axiom,
(N), is in its entirety expressible in three variables.
We incidentally get a proof that (W), when taken alone,
cannot be stated as a threevariable sentence: A fact announced in
Michael K. Kwatinetz' PhD thesis (1981), which however, to the
best of our knowledge, defeated proof attempts till now.
Key words:
Weak set theories, nvariable
expressibility, pebble games.

A. Formisano, E.G. Omodeo, and E. Orłowska.
A Prolog tool for relational translation of modal logics: a frontend
for relational proof systems. In Bernhard Beckert ed.,
TABLEAUX 2005 position papers and tutorial descriptions,
Universitaet KoblenzLandau, Fachberichte Informatik, 12/2005.
Abstract
Common approaches to automation of modal inferences usually
exploit ``ad hoc'' direct inference methods.
An alternative approach, aimed at developing a uniform relational platform for modal
reasoning,
is intended to
benefit from relational rendering of nonclassical logics.
The envisaged framework consist in a fullfledged inferential apparatus,
where the inferential activity can be seen as decomposed into two steps.
First, a translation phase brings from one (propositional) modal
formalization of a problem to its relational formulation. Then,
a deductive method is exploited, within the relational context,
in order to seek for a proof.
This paper is devoted to the first of these steps: we describe
a prototypical
implementation of a Prologbased tool able to uniformly translate
from various modal logics to the calculus of dyadic relations.
The adoption of a declarative programming approach
allows us to develop the system in an incremental way and ensures
high modularity and extensibility of the application.
At the moment the Prolog translator is able to produce
relational rendering of several modal logics.
We verified that our approach offers an high degree of uniformity:
we were able to treat varied modal logics by the very same machinery.
Moreover, extensions to further
classes of logics can easily be obtained by conservatively adding
suitable Prolog clauses.
Possible extensions of the tool are currently under design and development.
Key words:
Modal logic,
relation algebra,
translation methods,
tableaux,
sequent systems,
RasiowaSikorski systems

E.G. Omodeo, E. Orłowska, and A. Policriti.
RasiowaSikorski style Relational Elementary Set Theory.
In R. Berghammer, B. Möller, and George Struth eds.,
Proc. RelMiCS'7
and 2nd International Workshop on Applications of Kleene Algebra,
in combination with a workshop of the COST Action 274 (Malente, Germany, May 1217, 2003),
SpringerVerlag LNCS vol.3051, 215226, 2004.
Abstract
A RasiowaSikorski proof system is presented for an elementary set theory which can act
as a target language into which to translate propositional modal logics. The proposed system permits
the modular analysis of (modal) axioms in terms of deductive rules for the relational apparatus.
Such an analysis is possible even in the case when the starting modal logic does not possess
a firstorder correspondent. Moreover, the formalism enables a finetunable and uniform analysis
of modal deductions in a simple and purely settheoretic language.
Key words:
Modal logic, relational systems, translation methods.

A.Formisano,
E.G.Omodeo,
and
A.Policriti.
Threevariable statements of setpairing.
Denis Richard's anniversary issue (Patrick Cegielski ed.),
Theoretical
Computer Science, 322(1):147173, 2004.
Abstract
The approach to algebraic specifications of set theories proposed by Tarski and Givant inspires current research
aimed at taking advantage of the purely equational nature of the resulting formulations for enhanced
automation of reasoning on aggregates of various kinds: sets, bags, hypersets, etc. The viability of the said
approach rests upon the possibility to form pairs and to decompose them by means of conjugated projections.
Ordered pairs can be conceived of in many ways: along with the most classic one, several other pairing functions
are examined, which can be preferred to it when either the axiomatic assumptions are tooo weak to
enable pairing formation à la Kuratowski, or they are strong enough to make the specification
of conjugated projections particularly simple, and their formal properties easy to check within the calculus
of binary relations.
Key words:
Set theory, calculus of binary relations, pairing, automated reasoning, aggregates.

E.E. Doberkat and E.G. Omodeo.
ER modelling from first relational principles.
Theoretical
Computer Science, N.311(13), 285323, 2004.
Abstract
EntityRelationship (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 ERmodel 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 ERmodel 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 ERmodel represented in terms of the relation calculus.
Key words:
EntityRelationship models (static and dynamic view), relation algebra,
relational foundations of data modelling.

P. Caianiello, S.Costantini, and E.G. Omodeo. An
environment for specifying properties of dyadic relations and
reasoning about them. I: Language extension mechanisms. In H. de
Swart, E. Orłowska, G. Schmidt, and M. Roubens, eds., Theory
and Applications of Relational Structures as Knowledge
Instruments, SpringerVerlag, Lecture Notes in Computer Science,
vol.2929, 87106, 2003.

S.Costantini,
A.Formisano,
E.G.Omodeo. Mappings Between Domain Models in Answer Set Programming.
In Proceedings of the Joint Conference on Declarative Programming.
AGP03.
Reggio Calabria, Italy. September 35, 2003.

D.Cantone,
E.G.Omodeo, J.T. Schwartz, P.Ursino.
Notes from the logbook of a proofchecker's project. In N. Dershowitz ed.,
International symposium on verification (Theory and Practice)
celebrating Zohar Manna's 1000000_{2}th birthday. SpringerVerlag,
LNCS, vol.2772, pp.182207, 2003.

D.Cantone,
A.Formisano,
E.G.Omodeo, and J.T.Schwartz.
Various commonly occurring decidable
extensions of multilevel syllogistic. In S.Ranise and C.Tinelli, eds.,
Proceedings of the workshop on
Pragmatics of Decision Procedures in Automated Reasoning 2003
PDPAR'03 (CADE 19).
July 29, 2003 Miami, USA.

D.Cantone,
A.Formisano,
E.G.Omodeo,
and
C.G.Zarba.
Compiling dyadic firstorder specifications into map algebra.
Theoretical
Computer Science N.293(2), pp.447475, Feb.2003.

E.E. Doberkat and E.G. Omodeo.
Algebraic semantics of ERmodels in the context of the calculus of relations. II:
Dynamic view.
In H. de Swart ed., Relational methods in computer science, SpringerVerlag,
LNCS vol.2561, pp.5065, dec.2002.
A preprint available as
"Fachbereich Informatik, Lehrstuhls fuer SoftwareTechnologie,
MEMO Nr.114,
July 2001", and an extended abstract in H. de Swart ed.,
Proc. RelMiCS'6TARSKI,
Oisterwijk, the Netherlands, October 1621, 2001, pp.6276.

P. Caianiello,
S. Costantini,
and
E.G. Omodeo.
An environment for stepwise map specification and reasoning in Prolog. I:
Three language extension mechanisms.
In J.J. MorenoNavarro and J. Marino Carballo, eds.,
Proceedings of the Joint Conference on Declarative Programming.
AGP02.
Madrid, Spain, September 1618, 2002.

A. Formisano,
E.G. Omodeo,
and
A.Policriti.
Automation of aggregate theories:
The cornerstones of equational expressibility.
In J.J. MorenoNavarro and J. Marino Carballo, eds.,
Proceedings of the Joint Conference on Declarative Programming.
AGP02.
Madrid, Spain, September 1618, 2002.

A. Formisano,
E.G. Omodeo,
and
A.Policriti.
The axiom of elementary sets. II: The edge of Peircean
expressibility.
Research report n.20/02. Dipartimento di Matematica e
Informatica, Univ. di Perugia, 2002.

A. Formisano,
E.G. Omodeo,
and
A. Policriti.
The axiom of elementary sets. I: Threevariable
statements of setpairing.
Research report n.19/02. Dipartimento di Matematica
e Informatica, Univ. di Perugia, 2002.
 A.Formisano,
E.G.Omodeo,
and
A.Policriti.
Threevariable statements of setpairing.
Denis Richard 60th
Birthday Conference, Laboratoire de Logique, Algorithmique et Informatique
de ClermontFerrand, France, May 1617, 2002.
 E.G.Omodeo, and J.T.Schwartz. A modularization mechanism for interactive proofdevelopment.
Special Session on Automated Reasoning in Mathematics and Logic, J.G.F.Belinfante ed.,
2002AMS and MAA Spring Southeastern
Section Meeting, Atlanta, GA, March 810, 2002.
 A.Formisano,
E.G.Omodeo,
and
A.Policriti.
Automated validation of threevariable formulations of set pairing.
Special Session on Automated Reasoning in Mathematics and Logic, J.G.F.Belinfante ed.,
2002AMS and MAA Spring Southeastern
Section Meeting, Atlanta, GA, March 810, 2002.
(Also presented at
Workshop of WA2 and WA3,
April 1014, 2002, L'Aquila. Meeting of the project TARSKI, COST
Action N.274.)
 D. Cantone, E.G. Omodeo, and P. Ursino.
Formative processes with applications to the decision
problem in set theory: I. Powerset and singleton operators,
Information and Computation,
N.172, 165201, 2002.

E.G.Omodeo,
and
J.T.Schwartz,
A 'Theory' mechanism for a proofverifier based on firstorder set theory.
In: A. Kakas and F. Sadri (eds.), "Computational Logic: Logic Programming
and beyond", Essays in honour of Robert Kowalski, part II, SpringerVerlag,
Berlin. Lecture Notes in Artificial Intelligence, vol.2408, pp.214230, 2002.

D. Cantone,
E.G. Omodeo,
and
A.Policriti.
Set Theory for Computing  From decision procedures to declarative
programming with sets. SpringerVerlag,
Texts and Monographs in Computer Science, 2001.

A.Dovier,
A.Formisano,
and
E.G.Omodeo.
Decidability results for sets with atoms.
In L.M. Pereira and P. Quaresma, eds.,
Proceedings of the Joint Conference on Declarative Programming.
(AGP01) pp.245259,
Evora, Portugal, September 2628, 2001.

A. Formisano,
E.G.Omodeo,
and
A.Policriti.
The edge of 3variableinexpressibility beside Tarski's
Peircean formulation of setpairing.
In M. Pauly and G. Sandu eds., Proceedings of
ESSLLI Workshop on
Logic and Games, 2001.

A. Formisano,
E.G.Omodeo,
and
A.Policriti.
The axiom of elementary sets and Peircean expressibility.
In P. Cegielski ed.,
Vingtièmes Journées sur les Arithmétiques Faibles
 20th Weak Arithmetics Days,
June 56, 2001, IUT de Fontainebleau, France.

A. Formisano,
E.G.Omodeo,
and
M.Temperini.
Instructing equational setreasoning with Otter.
In R.Gore, A.Leitsch, and T.Nipkow eds.,
Automated
Reasoning.
Proc. of First International Joint Conference,
IJCAR 2001(CADE+FTP+TABLEAUX),
Lecture
Notes in Computer Science 2083, pages 152167,
SpringerVerlag, 2001.

A. Formisano,
E.G.Omodeo,
and
M.Temperini.
Layered map reasoning: An experimental approach put to trial on sets.
In A. Dovier, M.C. Meo, and A. Omicini Eds.,
Declarative Programming  Selected Papers from AGP 2000.
Electronic
Notes in Theoretical Computer Science, 48:128,
Elsevier Science B. V., 2001.

E.G. Omodeo and E.E. Doberkat.
Algebraic semantics of ERmodels in the context of the calculus of relations. I:
Static view.
In W. Kahl, D. L. Parnas, and G. Schmidt Eds.,
Proc. of Relational Methods in Software,
RelMiS 2001 (ETAPS 2001).
Electronic
Notes in Theoretical Computer Science, 44(3),
Elsevier Science B. V., 2001.
(Also in Bericht Nr.200102, Relational Methods in Software, RelMiS 2001.
Fakultaet
fuer
Informatik, Universitaet der Bundeswehr Muenchen. April, 2001.)

A. Formisano,
E.G.Omodeo,
and
M.Simeoni.
A graphical approach to relational reasoning.
In W. Kahl, D. L. Parnas, and G. Schmidt Eds.,
Proc. of Relational Methods in Software,
RelMiS 2001 (ETAPS 2001).
Electronic
Notes in Theoretical Computer Science, 44(3),
Elsevier Science B. V., 2001.
(Also in Bericht Nr.200102, Relational Methods in Software, RelMiS 2001.
Fakultaet
fuer
Informatik, Universitaet der Bundeswehr Muenchen. April, 2001.)

D.Cantone,
A.Formisano,
E.G.Omodeo,
and
C.G.Zarba,
Compiling dyadic firstorder specifications into map algebra.
Proceedings of the
16th Twente Workshop on Language Technology  2ndAMAST Workshop Algebraic
Methods in Language Processing
(AMILP
2000),
TWLT 16, University of Twente, pp.
3554, 2000.

A.Formisano
and
E.G.Omodeo.
Initial experiments in equational set reasoning.
AI*IANotizie, XIII(1), Periodico
dell'Associazione Italiana per
l'Intelligenza Artificiale, March 2000.

A.Chiacchiaretta,
A.Formisano,
and
E.G.Omodeo.
Map reasoning through existential multigraphs.
Report 05/00, Dipartimento di Matematica Pura ed Applicata,
Università di L'Aquila, April 2000.

A.Formisano,
E.G.Omodeo,
and
M.Temperini.
Goals and Benchmarks for Automated Map Reasoning.
J. of Symbolic
Computation,
29(2),
pp. 259297, February 2000.

A.Formisano,
and
E.G.Omodeo.
An equational reengineering of set theories.
In G.Salzer and R.Caferra eds.
Automated Deduction in Classical and NonClassical Logics.
Lecture
Notes in Computer Science 1761, pages 175190,
SpringerVerlag, Berlin, 2000.
(Extended version of FTP98).
 D. Cantone, E.G. Omodeo, and P. Ursino.
Formative processes with applications to the decision
problem in set theory: I. Powerset and singleton operators.
Technical Report 518 of IASI/CNR, Rome, Dec.1999.
 A. Dovier, E. Omodeo,
A. Policriti.
Solvable set/hyperset contexts: II. A goaldriven algorithm for the
blended case, Applicable Algebra in Engineering, Communication
and Computing (SpringerVerlag), 9(4):292332, 1999.

A.Chiacchiaretta,
A.Formisano,
and
E.G.Omodeo.
Benchmark #1 for equational set theory.
Associazione Italiana per l'Intelligenza
Artificiale (AI*IA),
giornata di lavori sul tema:
Analisi sperimentale di algoritmi per l'Intelligenza Artificiale.
December 1999. Roma, Italy.
Electronic proceedings in
http://www.dis.uniroma1.it/~rcra/roma99.
(Postscript).

D.Cantone,
A.Formisano,
E.G.Omodeo,
and
C.G.Zarba,
Compiling dyadic firstorder specifications into map
calculus, by folding quantifiers into map composition.
Research report 43/99, Department of Pure and Applied
Mathematics, University of L'Aquila, 1999.

A.Dovier,
A.Formisano,
and
E.G.Omodeo.
Provable $\exists^\ast\forall$sentences about sets with atoms.
In B. Jayaraman and G.F. Rossi, eds.,
Quaderni del Dipartimento di Matematica, n.200, pp.917,
Università di Parma.
Proceedings of the
DPS'99PLI'99,
Workshop on Declarative Programming with Sets.
Paris, France. September 27, 1999.
 D. Cantone,
E. G. Omodeo,
and
P. Ursino.
Transitive Venn diagrams with applications to the decision
problem in set theory,
Proceedings of the Joint Conference on Declarative Programming.
AGP99.
L'Aquila, Italy. September 69, 1999.

A.Formisano,
E.G.Omodeo,
and
M.Temperini.
Map Calculus: a link between algebraic specification and
firstorder theoremproving.
In proceedings of the
first workshop of the project `Sistemi formali per la specifica, l'analisi,
la verifica, la sintesi e la trasformazione di sistemi software'.
TFSiS98. Report SI98/11, DSI, Univ. "La Sapienza", Rome.
Centro Congressi dell'Università "La Sapienza", Rome. December 2123,
1998.

A.Formisano,
and
E.G.Omodeo.
An equational reengineering of set theories.
In G.Salzer and R.Caferra eds.
Proceedings of the International Workshop on
Firstorder Theorem Proving.
FTP98.
Technical Report E1852GS981,
Technische Universität Wien.
Schloss Wilhelminenberg, Wien, Austria. November 2325, 1998.

A.Formisano,
E.G.Omodeo,
and
M.Temperini.
Plan of Activities on the Map Calculus.
In J.L.FreireNistal, M.Falaschi and M.VilaresFerro eds. Proceedings of the
Joint Conference on Declarative Programming.
AGP98.
A Coruña, Spain. July 2023, 1998.
Abstract.

F.Aureli,
A.Formisano,
E.G.Omodeo,
and
M.Temperini.
Map Calculus: Initial application scenarios and experiments
based on Otter.
Report 466, IASICNR, 1998.
Abstract.