# Decision Procedures for Elementary Sublanguages of Set Theory. XVII. Commonly Occurring Decidable Extensions of Multi-level Syllogistic

## Abstract

The paper focuses on extending existing decision procedures for set theory and related theories commonly used in mathematics to handle such notions as monotonicity, ordering, inverse functions, etc. After presenting two decision procedures for the basic multilevel syllogistic fragment of set theory and studying the computational complexity of its decision problem, we illustrate a technique based on a syntactic translation of formulae with the special function and predicate symbols above into multilevel syllogistic that, in most cases, yields nondeterministic polynomial-time decision procedures. Such results can be quite useful for tool developers who aim at providing assistance to common mathematical reasoning. A semantically oriented approach is illustrated in the second part of the paper, where nondeterministic exponential-time decision procedures, of theoretical interest only, are briefly sketched for two extensions of multilevel syllogistic, with the general union operator and with the powerset operator.

## Keywords

Decision Procedure Extension Condition Satisfiability Problem Stabilization Step Initial Formula
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.

## References

1. 1.
Armando, A., Ranise, S., Rusinowitch, M.: Uniform derivation of decision procedures by superposition. In: Fribourg, L. (ed.) Proc. of Computer Science Logic 2001. LNCS, vol. 2142, pp. 513–527 (2001)
2. 2.
Breban, M., Ferro, A., Omodeo, E.G., Schwartz, J.T.: Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions. Commun. Pure Appl. Math. 34, 177–195 (1981)
3. 3.
Cantone, D.: Decision procedures for elementary sublanguages of set theory. X. Multilevel syllogistic extended by the singleton and powerset operators. J. Autom. Reason. 7(2), 193–230 (1991)
4. 4.
Cantone, D.: A fast saturation strategy for set-theoretic tableaux. In: Galmiche, D. (ed.) Proc. of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods. LNAI, vol. 1227, pp. 122–137. Springer, Berlin (1997)
5. 5.
Cantone, D., Cutello, V., Policriti, A.: Set-theoretic reductions of Hilbert’s tenth problem. In: Börger, E., Kleine Büning, H., Richter, M.M. (eds.) Proceedings of 3rd Workshop Computer Science Logic—CSL’89, Kaiserslautern, 1989, vol. 440, pp. 65–75. Springer, Berlin (1990) Google Scholar
6. 6.
Cantone, D., Ferro, A., Omodeo, E.G.: Computable Set Theory. Oxford Science Publications of International Series of Monographs in Computer Science, vol. 6. Clarendon Press, Oxford (1989)
7. 7.
Cantone, D., Ferro, A., Schwartz, J.T.: Decision procedures for elementary sublanguages of set theory. V. Multi-level syllogistic extended by the general union operator. J. Comput. Syst. Sci. 34(1), 1–18 (1987)
8. 8.
Cantone, D., Ferro, A., Schwartz, J.T.: Decision procedures for elementary sublanguages of set theory. VI. Multi-level syllogistic extended by the powerset operator. Commun. Pure Appl. Math. 38, 549–571 (1985)
9. 9.
Cantone, D., Longo, C., Nicolosi Asmundo, M.: A decidable quantified fragment of set theory involving ordered pairs with applications to description logics. In: Bezem, M. (ed.) Computer Science Logic (CSL’11)—25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, April 2011, vol. 12, pp. 129–143 (2011). Schloss Dagstuhl–Leibniz-Zentrum für Informatik Google Scholar
10. 10.
Cantone, D., Omodeo, E.G., Policriti, A.: The automation of syllogistic. II. Optimization and complexity issues. J. Autom. Reason. 6(2), 173–187 (1990)
11. 11.
Cantone, D., Omodeo, E.G., Policriti, A.: Set Theory for Computing. From Decision Procedures to Declarative Programming with Sets. Monographs in Computer Science. Springer, New York (2001)
12. 12.
Cantone, D., Omodeo, E.G., Schwartz, J.T., Ursino, P.: Notes from the logbook of a proof-checker’s project. In: Dershowitz, N. (ed.) Proc. of the International Symposium on Verification: theory and practice. LNCS, vol. 2772. Springer, Berlin (2012) Google Scholar
13. 13.
Cantone, D., Omodeo, E.G., Ursino, P.: Formative processes with applications to the decision problem in set theory: I. Powerset and singleton operators. Inf. Comput. 172, 165–201 (2002)
14. 14.
Cantone, D., Terranova, R., Ursino, P.: Experimental comparison of two tableau-based decision procedures for MLSS. In: CILC08—Convegno Italiano di Logica Computazionale, 10–12 July, Perugia (2008) Google Scholar
15. 15.
Cantone, D., Zarba, C.G., Schwartz, J.T.: A decision procedure for a sublanguage of set theory involving monotone, additive, and multiplicative functions, II: the multi-level case. Matematiche LX(1), 133–162 (2005)
16. 16.
Cantone, D., Zarba, C.G.: A new fast tableau-based decision procedure for an unquantified fragment of set theory. In: Caferra, R., Salzer, G. (eds.) Proc. of the International Workshop on First-Order Theorem Proving (FTP’98). LNAI, vol. 1761, pp. 126–136. Springer, Berlin (2000) Google Scholar
17. 17.
Ferro, A., Omodeo, E.G.: Decision procedures for elementary sublanguages of set theory. VII. Validity in set theory when a choice operator is present. Commun. Pure Appl. Math. 40, 265–280 (1987)
18. 18.
Ferro, A., Omodeo, E.G., Schwartz, J.T.: Decision procedures for elementary sublanguages of set theory. I. Multi-level syllogistic and some extensions. Commun. Pure Appl. Math. 33(5), 599–608 (1980)
19. 19.
Fitting, M.C.: First-Order Logic and Automated Theorem Proving, 2nd edn. Graduate Texts in Computer Science. Springer, Berlin (1996). 1st edn. (1990)
20. 20.
Formisano, A., Omodeo, E.G.: Theory-specific automated reasoning. In: Dovier, A., Pontelli, E. (eds.) A 25-Year Perspective on Logic Programming, pp. 37–63. Springer, Berlin (2010)
21. 21.
Omodeo, E.G.: The Ref proof-checker and its “common shared scenario”. This volume, pp. 121–167 (2012) Google Scholar
22. 22.
Omodeo, E.G., Cantone, D., Policriti, A., Schwartz, J.T.: A computerized referee. In: Schaerf, M., Stock, O. (eds.) Reasoning, Action and Interaction in AI Theories and Systems—Essays Dedicated to Luigia Carlucci Aiello. LNAI, vol. 4155, pp. 117–139. Springer, Berlin (2006)
23. 23.
Omodeo, E.G., Policriti, A.: The Bernays-Schönfinkel-Ramsey class for set theory: semidecidability. J. Symb. Log. 75(2), 459–480 (2010)
24. 24.
Omodeo, E.G., Policriti, A.: The Bernays-Schönfinkel-Ramsey class for set theory: decidability. J. Symbol. Log. (2012, to appear) Google Scholar
25. 25.
Omodeo, E.G., Schwartz, J.T.: A ‘Theory’ mechanism for a proof-verifier based on first-order set theory. In: Kakas, A., Sadri, F. (eds.) Computational Logic: Logic Programming and Beyond, Essays in Honour of Robert Kowalski, Part II. LNAI, vol. 2408, pp. 214–230. Springer, Berlin (2002) Google Scholar
26. 26.
Schwartz, J.T. (ed.): Mathematical Aspects of Computer Science. Proc. of Symposia in Applied Mathematics, vol. 19. Am. Math. Soc., Providence (1967)
27. 27.
Schwartz, J.T.: Set theory as a language for program specification and programming. Courant Institute of Mathematical Sciences, New York University (1970) Google Scholar
28. 28.
Schwartz, J.T.: A survey of program proof technology. Technical report 001, New York University, Department of Computer Science, September 1978 Google Scholar
29. 29.
Schwartz, J.T., Cantone, D., Omodeo, E.G.: Computational Logic and Set Theory: Applying Formalized Logic to Analysis. Springer, Berlin (2011). Foreword by M. Davis
30. 30.
Schwartz, J.T., Dewar, R.B., Schonberg, E., Dubinsky, E.: Programming with Sets: An Introduction to SETL. Springer, New York (1986)
31. 31.
Zarba, C.G., Cantone, D., Schwartz, J.T.: A decision procedure for a sublanguage of set theory involving monotone, additive, and multiplicative functions, I: the two-level case. J. Autom. Reason. 33(3–4), 251–269 (2004)