# Decision procedures for set/hyperset contexts

## Abstract

- (1)
Establishing whether a conjunction

*r*of formulae of the form ∀y_{1}... ∀y_{m}((y_{1}∃w_{1}& ...& y_{m}∃*w*_{ m })→q), with*q*unqualified and involving only the relators =, ∃ and propositional connectives, is satisfiable. - (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.

## Keywords

Free Variable Conjunctive Normal Form Unification Algorithm Finite Family Start Node## Preview

Unable to display preview. Download preview PDF.

## References

- 1.P. Aczel.
*Non-well-founded sets*. Vol 14, Lecture Notes, Center for the Study of Language and Information, Stanford, 1988.Google Scholar - 2.J. Barwise, J. Etchemendy.
*The liar: an essay on truth and circular propositions*. Oxford University Press, 1987.Google Scholar - 3.M. Beeson. Towards a computation system based on set theory. Theoretical Computer Science 60, 297–340, 1988.CrossRefGoogle Scholar
- 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.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.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.D. Cantone, A. Ferro, E.G. Omodeo.
*Computable set theory*, 1^{st}vol. Clarendon Press, Oxford, International Series of Monographs on Computer Science, 1989.Google Scholar - 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.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.B. Dreben, W. D. Goldfarb.
*The decision problem: solvable classes of quantificational formulas*. Addison-Wesley, 1979.Google Scholar - 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.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.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.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.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.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.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.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, 3^{rd}printing, 1977.Google Scholar - 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.J.W. Lloyd.
*Foundations of Logic Programming*. Springer-Verlag series*Symbolic Computation — Artificial Intelligence*, 2nd edition, 1987.Google Scholar - 21.Yu.I. Manin.
*A course in mathematical logic*. Springer-Verlag, New York, 1977.Google Scholar - 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.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.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.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.J.H. Siekmann. Unification Theory. A Survey.
*J. of Simbolic Computation*, 1989. Special Issue on Unification. 7(3,4) 8(1–5).Google Scholar