Decision procedures for set/hyperset contexts

  • Eugenio G. Omodeo
  • Alberto Policriti
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 722)


Pure, hereditarily finite, sets and hypersets are characterized both as an algorithmic data structure and by means of a first-order axiomatization which, although rather weak, suffices to make the following two problems decidable:
  1. (1)

    Establishing whether a conjunction r of formulae of the form ∀y1... ∀ym((y1∃w1 & ...& ymw m )→q), with q unqualified and involving only the relators =, ∃ and propositional connectives, is satisfiable.

  2. (2)

    Establishing whether a formula of the form ∀ y q, q as above, is satisfiable.


Concerning (1), an explicit decision algorithm is provided; moreover, significantly broad sub-problems of (1) are singled out in which a classification —named the ‘syllogistic decomposition’ of r — of all possible ways of satisfying the input conjunction r can be obtained automatically. For one of these sub-problems, carrying out the decomposition results in producing a finite family of syntactic substitutions that generate the space of all solutions to r. In this sense, one has a unification algorithm. Concerning (2), a technique is provided for reducing it to a sub-problem of (1) for which a decomposition method is available.


Free Variable Conjunctive Normal Form Unification Algorithm Finite Family Start Node 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    P. Aczel. Non-well-founded sets. Vol 14, Lecture Notes, Center for the Study of Language and Information, Stanford, 1988.Google Scholar
  2. 2.
    J. Barwise, J. Etchemendy. The liar: an essay on truth and circular propositions. Oxford University Press, 1987.Google Scholar
  3. 3.
    M. Beeson. Towards a computation system based on set theory. Theoretical Computer Science 60, 297–340, 1988.CrossRefGoogle Scholar
  4. 4.
    S. Baratella, R. Ferro. A theory of sets with the negation of the axiom of infinity. AILA preprints n.8, 1991.Google Scholar
  5. 5.
    M. Breban, A. Ferro, E.G. Omodeo, J.T. Schwartz. Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions. Comm. on Pure and Appl. Mathematics, 34, 177–195, 1981.Google Scholar
  6. 6.
    R. Boyer, E. Lusk, W. McCune, R. Overbeek, M. Stickel, L. Wos. Set theory in first-order logic: Clauses for Gödel's axioms. J. of Automated Reasoning, 2, 289–327, 1986.Google Scholar
  7. 7.
    D. Cantone, A. Ferro, E.G. Omodeo. Computable set theory, 1st vol. Clarendon Press, Oxford, International Series of Monographs on Computer Science, 1989.Google Scholar
  8. 8.
    D. Cantone, S. Ghelfo, E.G. Omodeo. The automation of syllogistic. I. Syllogistic normal forms. J. of Symbolic Computation, 6(1), 83–98, 1988.Google Scholar
  9. 9.
    D. Cantone, E.G. Omodeo, A. Policriti. The automation of syllogistic. II. Optimization and complexity issues. J. of Automated Reasoning, Kluwer Academic Publishers, 6(2), 173–187, 1990.Google Scholar
  10. 10.
    B. Dreben, W. D. Goldfarb. The decision problem: solvable classes of quantificational formulas. Addison-Wesley, 1979.Google Scholar
  11. 11.
    R. Dionne, E. Mays, F.J. Oles. A non-well-founded approach to terminological cycles. Proceedings of AAAI-92, San Jose, Cal.Google Scholar
  12. 12.
    R. Dionne, E. Mays, F.J. Oles. The equivalence of model-theoretic and structural subsumption in description logics. To appear in the proceedings of IJCAI-93.Google Scholar
  13. 13.
    A. Dovier, E.G. Omodeo, E. Pontelli, G. Rossi. {log}: a logic programming language with finite sets. In K. Furukawa ed., Logic Programming, Proceedings of the Eighth International Conference (ICLP'91, Paris), The MIT Press, 111–124, 1991.Google Scholar
  14. 14.
    A. Dovier, E.G. Omodeo, E. Pontelli, G.-F. Rossi. Embedding finite sets in a logic programming language. In E. Lamma, P. Mello eds, Extensions of Logic Programming, Volume 660 of Lecture Notes in Artificial Intelligence, 150–167, Springer-Verlag, 1993.Google Scholar
  15. 15.
    M. Forti, F. Honsell. Set theory with free construction principles. Annali Scuola Normale Superiore di Pisa, Cl. Sc. (IV)10, 493–522, 1983.Google Scholar
  16. 16.
    A. Ferro, E.G. Omodeo, J.T. Schwartz. Decision procedures for elementary sublanguages of set theory. I. Multi-level syllogistic and some extensions. Communications on Pure and Applied Mathematics, 33, 599–608, 1980.Google Scholar
  17. 17.
    M.R. Garey, D.S. Johnson. Computers and intractability — A Guide to the theory of NP-Completeness. W.H. Freeman and Co., New York, A series of books in the mathematical sciences, 1979.Google Scholar
  18. 18.
    J. v. Heijenoort, editor. From Frege to Gödel — A source book in mathematical logic, 1879–1931. Harvard University Press, Source books in the history of the sciences, 3rd printing, 1977.Google Scholar
  19. 19.
    J.P. Jouannaud, C. Kirchner. Solving equations in abstract algebras: a rule-based survey of unification. In J.-L. Lassez, G. Plotkin eds., Alan Robinson's anniversary book, 1991.Google Scholar
  20. 20.
    J.W. Lloyd. Foundations of Logic Programming. Springer-Verlag series Symbolic Computation — Artificial Intelligence, 2nd edition, 1987.Google Scholar
  21. 21.
    Yu.I. Manin. A course in mathematical logic. Springer-Verlag, New York, 1977.Google Scholar
  22. 22.
    A. Martelli, U. Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems (TOPLAS), 4(2), 258–282, 1982.CrossRefGoogle Scholar
  23. 23.
    E.G. Omodeo, F. Parlamento, A. Policriti. Decidability of ∃*∀-sentences in membership theories. University of Udine Research Report Nr.6, May 1992.Google Scholar
  24. 24.
    E.G. Omodeo, F. Parlamento, A. Policriti. A derived algorithm for evaluating ε-expressions over sets. Univ. of Rome “La Sapienza”-D.I.S., Rep.07.92 May 1992. (To appear on the J. of Symbolic Computation, special issue on automatic programming).Google Scholar
  25. 25.
    J.T. Schwartz, R.K.B. Dewar, E. Dubinsky, E. Schonberg. Programming with sets- An introduction to SETL. Texts and Monographs in Computer Science, Springer-Verlag, 1986.Google Scholar
  26. 26.
    J.H. Siekmann. Unification Theory. A Survey. J. of Simbolic Computation, 1989. Special Issue on Unification. 7(3,4) 8(1–5).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Eugenio G. Omodeo
    • 1
  • Alberto Policriti
    • 2
  1. 1.Dip. di Informatica e SistemisticaUniversità di Roma “La Sapienza”Roma
  2. 2.Dip. di Matematica e InformaticaUniversità di UdineUdineItaly

Personalised recommendations