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

Ferro Inferential Core 

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) CrossRefGoogle Scholar
  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) MathSciNetMATHCrossRefGoogle Scholar
  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) MathSciNetMATHGoogle Scholar
  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) CrossRefGoogle Scholar
  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) MATHGoogle Scholar
  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) MathSciNetMATHCrossRefGoogle Scholar
  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) MathSciNetMATHCrossRefGoogle Scholar
  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) MathSciNetMATHCrossRefGoogle Scholar
  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) MATHGoogle Scholar
  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) MathSciNetMATHCrossRefGoogle Scholar
  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) MathSciNetGoogle Scholar
  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) MathSciNetMATHCrossRefGoogle Scholar
  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) MathSciNetMATHCrossRefGoogle Scholar
  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) MATHCrossRefGoogle Scholar
  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) CrossRefGoogle Scholar
  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) CrossRefGoogle Scholar
  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) MathSciNetMATHCrossRefGoogle Scholar
  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) MATHGoogle Scholar
  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 MATHGoogle Scholar
  30. 30.
    Schwartz, J.T., Dewar, R.B., Schonberg, E., Dubinsky, E.: Programming with Sets: An Introduction to SETL. Springer, New York (1986) MATHGoogle Scholar
  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) MathSciNetMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag London 2013

Authors and Affiliations

  1. 1.Dipartimento di Matematica e InformaticaUniversità di CataniaCataniaItaly

Personalised recommendations