A decision procedure for a satisfiability problem in a hereditarily finite set-theoretical universe. (Une procédure de décision pour un problème de satisfiabilité dans un univers ensembliste héréditairement fini.) (French) Zbl 0889.68062

Summary: We deal with the satisfiability problem for systems of constraints over hereditarily finite sets. This problem is central for integrating sets in programming languages, and particularly for constraint logic programming languages. The approach we propose here is based on reducing systems of set constraints into systems of linear integer equalities and inequalities (with bounded domain). The complexity of the reduction is on \(O(n^3)\).


68Q15 Complexity classes (hierarchies, relations among complexity classes, etc.)
68N17 Logic programming
03C15 Model theory of denumerable and separable structures


Full Text: DOI EuDML


[1] 1. A. AIKEN et E. WIMMERS, Solving Systems of Set Constraints, In 7th Symposium on LICS, 1992. · Zbl 0834.68105
[2] 2. A. AIKEN, D. KOZEN et E. WIMMERS, Decidability of Systems of Set Constraints with Negative Constraints, Technical Report 93-1362, Computer Science Departement, Cornell University, June 1993. · Zbl 0834.68105
[3] 3. F. AMBERT, B. LEGEARD et E. LEGROS, Constraint Logic Programming on Sets and Multisets, Workshop on Constraint Languages and their usein Problem modelling, in conjunction with ILPS’94, Ithaca, USA, pp. 151-165, November 18, 1994.
[4] 4. C. BEERI, S. NAQVI, R. RAMAKRISHNAN, O. SHMUELI, S. TSUR, Sets and negation in a logic database language (LDL1), Proceedings of the 6th Annual ACM SIGMOD Symposium on principles of Database Systems, 1987, 16, N3, pp.21-37.
[5] 5. F. M. BROWN, Towards the Automation of Set Theory and its Logic, Artificial Intelligence, 1978, 10, pp.281-316. Zbl0395.68082 MR514045 · Zbl 0395.68082 · doi:10.1016/S0004-3702(78)80017-4
[6] 6. D. CANTONE, A. FERRO et E. OMODEO, Computable Set Theory, Academic Press 1990. Zbl0755.03024 · Zbl 0755.03024
[7] 7. A. COLMERAUER, An Introduction to PROLOG III, In Communication of the A.C.M., July 1990, 33, No. 7. · Zbl 0679.68045
[8] 8. D. CANTONE, E. OMODEO et A. POLICRITI, The Automation of Syllogistic II. Optimization and Complexity Issues, Journal of Automated Reasoning, 1990, 6, pp. 173-187. Zbl0744.03015 MR1066797 · Zbl 0744.03015 · doi:10.1007/BF00245817
[9] 9. M. DINCBAS, P. VAN HENTERYCK, H. SIMONIS, A. AGGOUN, T. GRAF et F. BERTHIER, The Constraint Logic Programming Language CHIP, Proceeding of the International Conference on Fifth generation Computer System (Tokyo88).
[10] 10. A. DOVIER, E. OMODEO, E. PONTELLI et G. F. ROSSI, log: A Logic Programming Language With Finite Sets, Proceedings of The Eighth International Conference in Logic Programming (K.Furukawa, ed), The MIT Press, 1991, p. 111-124. · Zbl 0874.68056
[11] 11. A. FERRO, E. OMODEO et J. T. SCHWARTZ, Decision Procedures for Elementary Sublanguages of Set Theory. I: Multi-level syllogistic andsome Extensions, Comm. Pure and Appl. Math., 1980, XXXIII, pp. 599-608. Zbl0453.03009 MR586413 · Zbl 0453.03009 · doi:10.1002/cpa.3160330503
[12] 12. R. GILLERON, S. TISON et M. TOMMASI, Solving Systems of Set Constraints using Tree Automata, In Proc. STACS, LNCS 665, Février 1993, Springer-Verlag, p. 505-514. Zbl0797.68115 MR1249313 · Zbl 0797.68115
[13] 13. N. HEINTZ et J. JAFFAR, A Decision Procedure fora Class of Set Constraints, LICS 90.
[14] 14. M. HIBTI, NP-Complétude du langage MLS, Mémoire de DEA de Mathématiques, Université de Franche-Comté, Septembre 1991.
[15] 15. M. HIBTI, Satisfiabilité dans certains langages ensemblistes, Actes de la journée ensemble, rapport de recherche LIFO Orléans, 9 avril 1992.
[16] 16. M. HIBTI, Décidabilité et Complexité de systèmes de contraintes ensemblistes, Thèse de Doctorat de Mathématiques, Université de Franche-Comté, N d’ordre 464, juin 1995.
[17] 17. M. HIBTI, H. LOMBARDI et B. LEGEARD, Deciding in HFS-Theory via Linear Integer Programming with Application to Set-Unification, in Proc. of the 4th International Conference on Logic Programming and Automated Reasoning LPAR 93, St Petersbourg, pp. 170-181, Springer LNCS 698. Zbl0790.90052 MR1251075 · Zbl 0790.90052
[18] 18. M. HIBTI, B. LEGEARD et H. LOMBARDI, Decision Procedure for Constraintsover Sets Multisets and Sequences, Research report LAB-RRIAP 9402. · Zbl 0889.68062
[19] 19. J. JAFFAR et J. L. LASSEZ, Constraint Logic Programming, Proceedings of the 14th ACM Conference on Principle of Programming Languages, POPL, Munich, 1987, pp. 111-119.
[20] 20. J. JAFFAR et M. K. MAHER, Constraint Logic Programming: A Survey, J. of Logic Programming, May/July, 1994, 19/20, pp. 503-582. MR1279934 · Zbl 0900.68127
[21] 21. D. KAPUR et P. NARENDRAN, NP-Completeness of the Set Unification and Matching Problems, Proc. of the ICAD, Oxford, July 1986, Springer LNCS 230, 489-495. Zbl0643.68054 MR876524 · Zbl 0643.68054
[22] 22. G. M. KUPER, Logic Programming with Sets, Research Report IBM Yorktown Heights, RC 12378, Dec. 1987.
[23] 23. B. LEGEARD, H. LOMBARDI, E. LEGROS et M. HIBTI, A Satisfaction Approach to Set Unification, in Proceedings of the 13th International Conference on Artificial Intelligence, Expert Systems and Natural Language, EC2, Avignon, 1993, 1, pp. 265-276.
[24] 24. A. K. MACKWORTH, ”Consistency in Network of Relations”, Journal of Artificial Intelligence, 1977, 8, n^\circ 1, pp.99-118. Zbl0341.68061 · Zbl 0341.68061 · doi:10.1016/0004-3702(77)90007-8
[25] 25. B. A. NADEL, Constraints Satisfaction Algorithms, Journal of Computer Intelligence, 1989, 5, pp. 188-224.
[26] 26. A. POLICRITI, NP-completeness of MLS, technical report, University of Udine, 1990.
[27] 27. F. PARLAMENTO et A. POLICRITI, Decision Procedures for Elementary Sub-languages of Set Theory. XIII: Model Graph, Reflexion and Decidability, Journal of Automated Reasoning, 1991, 7. Zbl0734.03006 MR1118329 · Zbl 0734.03006 · doi:10.1007/BF00243810
[28] 28. F. PARLAMENTO et A. POLICRITI, Undecidability Results for Restricted Universallu Quantified Formulae of Set Theory, Com. on Pure and Applied Mathematics, 1993, XLVI, pp. 57-73. Zbl0797.03005 MR1193343 · Zbl 0797.03005 · doi:10.1002/cpa.3160460104
[29] 29. D. PASTRE, Automatic Theorem Proving in Set Theory, Artificial Intelligence, 1978, 10, pp. 1-27. Zbl0374.68059 MR496431 · Zbl 0374.68059 · doi:10.1016/0004-3702(78)90028-0
[30] 30. K. J. PERRY, K. V. PALEM, K. MCALOON et G. M. KUPER, The Complexity of Logic Programming with Sets, Research Report IBM Yorktown Heights, RC 12887, 1987. · Zbl 0784.68042
[31] 31. J. H. SIEKMANN, Unification Theory, in Unification, Edited by C. Kirchner, Academic Press, 1990, pp. 1-68. MR1090370 · Zbl 0704.68096
[32] 32. R. SIGAL, Desiderata for Logic Programming with Sets, GULP Proceedings of the 4th National Conference on Logic Programming, 1989, pp. 127-141, Bologna.
[33] 33. Y. SATO, K. SAKAI et S. MENJU, SetCAL- a Solver of Set Constraints in CAL System, Technical Report TM-0963, ICOT, 1990.
[34] 34. J. T. SCHWARTS, R. B. DEWAR, E. DUBINSKY et E. SCHONBERG, Programming with Sets - An Introduction to SETL, 493 pages, Springer-Verlag Editions, Berlin, 1986. Zbl0604.68001 · Zbl 0604.68001
[35] 35. E. TSANG, Foundations of Constraint Satisfaction, Academic Press, 1993.
[36] 36. P. VAN HENTENRYCK, Constraint Satisfaction in Logic Programming, The MIT Press, 224 pages, 1989. MR1013366 · Zbl 0707.68101
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.