Quantifier Elimination in Elementary Set Theory

  • Ewa Orłowska
  • Andrzej Szałas
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3929)


In the current paper we provide two methods for quantifier elimination applicable to a large class of formulas of the elementary set theory. The first one adapts the Ackermann method [1] and the second one adapts the fixpoint method of [20]. We show applications of the proposed techniques in the theory of correspondence between modal logics and elementary set theory. The proposed techniques can also be applied in an automated generation of proof rules based on the semantic-based translation of axioms of a given logic into the elementary set theory.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Ackermann, W.: Untersuchungen über das Eliminationsproblem der Mathematischen Logik. Mathematische Annalen 110, 390–413 (1935)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Arnold, A., Niwinski, D.: Rudiments of μ-calculus. Studies in Logic and the Foundations of Mathematics. Elsevier, Amsterdam (2001)zbMATHGoogle Scholar
  3. 3.
    Berghammer, R., Möller, B., Struth, G. (eds.): RelMiCS 2003. LNCS, vol. 3051. Springer, Heidelberg (2004)zbMATHGoogle Scholar
  4. 4.
    D’Agostino, G., Montanari, A., Policriti, A.: A set-theoretic translation method for polymodal logics. Journal of Automated Reasoning 3(15), 317–337 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Demri, S., Orłowska, E.: Logical analysis of demonic nondeterministic programs. Theoretical Computer Science 166, 173–202 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Doherty, P., Kachniarz, J., Szałas, A.: Using contextually closed queries for local closed-world reasoning in rough knowledge databases. In: Pal, S.K., Polkowski, L., Skowron, A. (eds.) Rough-Neuro Computing: Techniques for Computing with Words, pp. 219–250. Springer, Heidelberg (2003)Google Scholar
  7. 7.
    Doherty, P., Łukaszewicz, W., Szałas, A.: Computing circumscription revisited. Journal of Automated Reasoning 18(3), 297–336 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Doherty, P., Łukaszewicz, W., Szałas, A.: Declarative PTIME queries for relational databases using quantifier elimination. Journal of Logic and Computation 9(5), 739–761 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Doherty, P., Łukaszewicz, W., Szałas, A.: Computing strongest necessary and weakest sufficient conditions of first-order formulas. In: International Joint Conference on AI (IJCAI 2001), pp. 145–151 (2000)Google Scholar
  10. 10.
    Düntsch, I., Orłowska, E.: A proof system for contact relation algebras. Journal of Philosophical Logic 29, 241–262 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Frias, M., Orłowska, E.: A proof system for fork algebras and its applications to reasoning in logics based on intuitionism. Logique et Analyse 150, 151, 152, 239–284 (1995)Google Scholar
  12. 12.
    Gabbay, D.M., Ohlbach, H.J.: Quantifier elimination in second-order predicate logic. In: Nebel, B., Rich, C., Swartout, W. (eds.) Principles of Knowledge representation and reasoning, KR 1992, pp. 425–435. Morgan Kaufmann, San Francisco (1992)Google Scholar
  13. 13.
    Kachniarz, J., Szałas, A.: On a static approach to verification of integrity constraints in relational databases. In: [29], pp. 97–109 (2001)Google Scholar
  14. 14.
    Knaster, B.: Un theoreme sur les fonctions d’ensembles. Ann. Soc. Polon. Math. 6, 133–134 (1928)zbMATHGoogle Scholar
  15. 15.
    Konikowska, B., Orłowska, E.: A relational formalisation of a generic many-valued modal logic. In: [29], pp. 183–202 (2001)Google Scholar
  16. 16.
    Lifschitz, V.: Computing circumscription. In: Proc. 9th IJCAI, pp. 229–235. Morgan Kaufmann, San Francisco (1985)Google Scholar
  17. 17.
    Lifschitz, V.: Circumscription. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Artificial Intelligence and Logic Programming, vol. 3, pp. 297–352. Oxford University Press, Oxford (1991)Google Scholar
  18. 18.
    MacCaull, W., Orłowska, E.: Correspondence results for relational proof systems with application to the Lambek calculus. Studia Logica: an International Journal for Symbolic Logic 71(3), 279–304 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Nonnengart, A., Ohlbach, H.J., Szałas, A.: Elimination of predicate quantifiers. In: Ohlbach, H.J., Reyle, U. (eds.) Logic, Language and Reasoning. Essays in Honor of Dov Gabbay, Part I, pp. 159–181. Kluwer, Dordrecht (1999)Google Scholar
  20. 20.
    Nonnengart, A., Szałas, A.: A fixpoint approach to second-order quantifier elimination with applications to correspondence theory. In: Orłowska, E. (ed.) Logic at Work: Essays Dedicated to the Memory of Helena Rasiowa. Studies in Fuzziness and Soft Computing, vol. 24, pp. 307–328. Springer, Physical-verlag (1998)Google Scholar
  21. 21.
    Omodeo, E., Orłowska, E., Policriti, A.: Rasiowa-Sikorski style relational elementary set theory. In: Berghammer, R., Moeller, B., Struth, G. (eds.) [3], pp. 213–224 (2004)Google Scholar
  22. 22.
    Orłowska, E.: Dynamic logic with program specifications and its relational proof system. Journal of Applied Non-Classical Logic 3, 147–171 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Orłowska, E.: Relational interpretation of modal logics. In: Andreka, H., Monk, D., Nemeti, I. (eds.) Algebraic Logic. Colloquia Mathematica Societatis Janos Bolyai, vol. 54, pp. 443–471 (1988)Google Scholar
  24. 24.
    Orłowska, E.: Relational proof systems for relevant logics. Journal of Symbolic Logic 57, 1425–1440 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Orłowska, E.: Relational semantics for non-classical logics: Formulas are relations. In: Woleński, J. (ed.) Philosophical Logic in Poland, pp. 167–186 (1994)Google Scholar
  26. 26.
    Orłowska, E.: Relational proof systems for modal logics. In: Wansing, H. (ed.) Proof Theory of Modal Logics, pp. 55–77 (1996)Google Scholar
  27. 27.
    Orłowska, E.: Relational formalisation of nonclassical logics. In: Brink, C., Kahl, W., Schmidt, G. (eds.) Relational Methods in Computer Science, pp. 90–105 (1997)Google Scholar
  28. 28.
    Orłowska, E., McCaull, W.: A calculus of typed relations. In: [3], pp. 152–158 (2004)Google Scholar
  29. 29.
    Orłowska, E., Szałas, A. (eds.): Relational Methods for Computer Science Applications. Springer, Heidelberg (2001)zbMATHGoogle Scholar
  30. 30.
    Simmons, H.: The monotonous elimination of predicate variables. Journal of Logic and Computation 4, 23–68 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Szałas, A.: On the correspondence between modal and classical logic: An automated approach. Journal of Logic and Computation 3, 605–620 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  32. 32.
    Szałas, A.: On an automated translation of modal proof rules into formulas of the classical logic. Journal of Applied Non-Classical Logics 4, 119–127 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  33. 33.
    Szałas, A.: Second-order quantifier elimination in modal contexts. In: Flesca, S., Greco, S., Leone, N., Ianni, G. (eds.) JELIA 2002. LNCS (LNAI), vol. 2424, pp. 223–232. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  34. 34.
    Szałas, A.: On a logical approach to estimating computational complexity of potentially intractable problems. In: Lingas, A., Nilsson, B.J. (eds.) FCT 2003. LNCS, vol. 2751, pp. 423–431. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  35. 35.
    Tarski, A.: A Lattice-theoretical Fixpoint Theorem and its Applications. Pacific Journal of Mathematics 5(2), 285–309 (1965)MathSciNetCrossRefzbMATHGoogle Scholar
  36. 36.
    van Benthem, J.: Modal Logic and Classical Logic. Bibliopolis, Naples (1983)Google Scholar
  37. 37.
    van Benthem, J.: Correspondence theory. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 2, pp. 167–247. D. Reidel Pub. Co., Dordrecht (1984)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Ewa Orłowska
    • 1
  • Andrzej Szałas
    • 2
    • 3
  1. 1.National Institute of TelecommunicationsWarsawPoland
  2. 2.The University of Economics and Computer ScienceOlsztynPoland
  3. 3.Department of Information and Computer ScienceUniversity of LinköpingSweden

Personalised recommendations