Recent publications coauthored by Eugenio Omodeo

• J.T. Schwartz D. Cantone, and E.G. Omodeo, . Springer-Verlag, 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 theory-based 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)269-301, 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 goal-driven algorithms. An alternative approach to modeling atoms, that allows one to retain the original formulation of extensionality, was proposed by Quine: atoms are self-singletons. 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 goal-driven unification algorithm.

  Key words:

  Set-hyperset 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):953-968, 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 single-element adjunction and removal, (W) and (L), cannot be axiomatized by means of three-variable 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 three-variable 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, n-variable expressibility, pebble games.

• A. Formisano, E.G. Omodeo, and E. Orłowska. A Prolog tool for relational translation of modal logics: a front-end for relational proof systems. In Bernhard Beckert ed., TABLEAUX 2005 position papers and tutorial descriptions, Universitaet Koblenz-Landau, 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 non-classical logics. The envisaged framework consist in a full-fledged 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 Prolog-based 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, Rasiowa-Sikorski systems

• E.G. Omodeo, E. Orłowska, and A. Policriti. Rasiowa-Sikorski 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 12-17, 2003), Springer-Verlag LNCS vol.3051, 215--226, 2004.

  Abstract

  A Rasiowa-Sikorski 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 first-order correspondent. Moreover, the formalism enables a fine-tunable and uniform analysis of modal deductions in a simple and purely set-theoretic language.

  Key words:

  Modal logic, relational systems, translation methods.

• A.Formisano, E.G.Omodeo, and A.Policriti. Three-variable statements of set-pairing. Denis Richard's anniversary issue (Patrick Cegielski ed.), Theoretical Computer Science, 322(1):147-173, 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(1-3), 285-323, 2004.

  Abstract

  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.

  Key words:

  Entity-Relationship 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, Springer-Verlag, Lecture Notes in Computer Science, vol.2929, 87--106, 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 3-5, 2003.
• D.Cantone, E.G.Omodeo, J.T. Schwartz, P.Ursino. Notes from the logbook of a proof-checker's project. In N. Dershowitz ed., International symposium on verification (Theory and Practice) celebrating Zohar Manna's 1000000₂-th birthday. Springer-Verlag, LNCS, vol.2772, pp.182-207, 2003.
• D.Cantone, A.Formisano, E.G.Omodeo, and J.T.Schwartz. Various commonly occurring decidable extensions of multi-level 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 first-order specifications into map algebra. Theoretical Computer Science N.293(2), pp.447-475, Feb.2003.
• E.-E. Doberkat and E.G. Omodeo. Algebraic semantics of ER-models in the context of the calculus of relations. II: Dynamic view. In H. de Swart ed., Relational methods in computer science, Springer-Verlag, LNCS vol.2561, pp.50-65, dec.2002. A preprint available as "Fachbereich Informatik, Lehrstuhls fuer Software-Technologie, MEMO Nr.114, July 2001", and an extended abstract in H. de Swart ed., Proc. RelMiCS'6-TARSKI, Oisterwijk, the Netherlands, October 16-21, 2001, pp.62-76.
• 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. Moreno-Navarro and J. Marino Carballo, eds., Proceedings of the Joint Conference on Declarative Programming. AGP02. Madrid, Spain, September 16-18, 2002.
• A. Formisano, E.G. Omodeo, and A.Policriti. Automation of aggregate theories: The cornerstones of equational expressibility. In J.J. Moreno-Navarro and J. Marino Carballo, eds., Proceedings of the Joint Conference on Declarative Programming. AGP02. Madrid, Spain, September 16-18, 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: Three-variable statements of set-pairing. Research report n.19/02. Dipartimento di Matematica e Informatica, Univ. di Perugia, 2002.
• A.Formisano, E.G.Omodeo, and A.Policriti. Three-variable statements of set-pairing. Denis Richard 60th Birthday Conference, Laboratoire de Logique, Algorithmique et Informatique de Clermont-Ferrand, France, May 16-17, 2002.
• E.G.Omodeo, and J.T.Schwartz. A modularization mechanism for interactive proof-development. Special Session on Automated Reasoning in Mathematics and Logic, J.G.F.Belinfante ed., 2002-AMS and MAA Spring Southeastern Section Meeting, Atlanta, GA, March 8-10, 2002.
• A.Formisano, E.G.Omodeo, and A.Policriti. Automated validation of three-variable formulations of set pairing. Special Session on Automated Reasoning in Mathematics and Logic, J.G.F.Belinfante ed., 2002-AMS and MAA Spring Southeastern Section Meeting, Atlanta, GA, March 8-10, 2002. (Also presented at Workshop of WA2 and WA3, April 10-14, 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, 165-201, 2002.
• E.G.Omodeo, and J.T.Schwartz, A 'Theory' mechanism for a proof-verifier based on first-order set theory. In: A. Kakas and F. Sadri (eds.), "Computational Logic: Logic Programming and beyond", Essays in honour of Robert Kowalski, part II, Springer-Verlag, Berlin. Lecture Notes in Artificial Intelligence, vol.2408, pp.214-230, 2002.
• D. Cantone, E.G. Omodeo, and A.Policriti. Set Theory for Computing - From decision procedures to declarative programming with sets. Springer-Verlag, 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.245-259, Evora, Portugal, September 26-28, 2001.
• A. Formisano, E.G.Omodeo, and A.Policriti. The edge of 3-variable-inexpressibility beside Tarski's Peircean formulation of set-pairing. 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 5-6, 2001, IUT de Fontainebleau, France.
• A. Formisano, E.G.Omodeo, and M.Temperini. Instructing equational set-reasoning 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 152-167, Springer-Verlag, 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:1-28, Elsevier Science B. V., 2001.
• E.G. Omodeo and E.-E. Doberkat. Algebraic semantics of ER-models 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.2001-02, 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.2001-02, 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 first-order specifications into map algebra. Proceedings of the 16th Twente Workshop on Language Technology - 2nd-AMAST Workshop Algebraic Methods in Language Processing (AMILP 2000), TWLT 16, University of Twente, pp. 35-54, 2000.
• A.Formisano and E.G.Omodeo. Initial experiments in equational set reasoning. AI*IA-Notizie, 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. 259-297, February 2000.
• A.Formisano, and E.G.Omodeo. An equational re-engineering of set theories. In G.Salzer and R.Caferra eds. Automated Deduction in Classical and Non-Classical Logics. Lecture Notes in Computer Science 1761, pages 175-190, Springer-Verlag, 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 goal-driven algorithm for the blended case, Applicable Algebra in Engineering, Communication and Computing (Springer-Verlag), 9(4):292-332, 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 first-order 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.9-17, Università di Parma. Proceedings of the DPS'99-PLI'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 6-9, 1999.
• A.Formisano, E.G.Omodeo, and M.Temperini. Map Calculus: a link between algebraic specification and first-order theorem-proving. 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 SI-98/11, DSI, Univ. "La Sapienza", Rome. Centro Congressi dell'Università "La Sapienza", Rome. December 21-23, 1998.
• A.Formisano, and E.G.Omodeo. An equational re-engineering of set theories. In G.Salzer and R.Caferra eds. Proceedings of the International Workshop on First-order Theorem Proving. FTP98. Technical Report E1852-GS-981, Technische Universität Wien. Schloss Wilhelminenberg, Wien, Austria. November 23-25, 1998.
• A.Formisano, E.G.Omodeo, and M.Temperini. Plan of Activities on the Map Calculus. In J.L.Freire-Nistal, M.Falaschi and M.Vilares-Ferro eds. Proceedings of the Joint Conference on Declarative Programming. AGP98. A Coruña, Spain. July 20-23, 1998. Abstract.
• F.Aureli, A.Formisano, E.G.Omodeo, and M.Temperini. Map Calculus: Initial application scenarios and experiments based on Otter. Report 466, IASI-CNR, 1998. Abstract.