Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Quantifier Elimination in Elementary Set Theory

  • Conference paper
Relational Methods in Computer Science (RelMiCS 2005)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3929))

Included in the following conference series:

Abstract

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.

Partially supported by the EU Cost Action 274 (Tarski), INTAS project 04-77-7080 and the grant 3 T11C 023 29 of the Polish Ministry of Science and Information Society Technologies.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Ackermann, W.: Untersuchungen über das Eliminationsproblem der Mathematischen Logik. Mathematische Annalen 110, 390–413 (1935)

    Article  MathSciNet  MATH  Google Scholar 

  2. Arnold, A., Niwinski, D.: Rudiments of μ-calculus. Studies in Logic and the Foundations of Mathematics. Elsevier, Amsterdam (2001)

    MATH  Google Scholar 

  3. Berghammer, R., Möller, B., Struth, G. (eds.): RelMiCS 2003. LNCS, vol. 3051. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  5. Demri, S., Orłowska, E.: Logical analysis of demonic nondeterministic programs. Theoretical Computer Science 166, 173–202 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  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. Doherty, P., Łukaszewicz, W., Szałas, A.: Computing circumscription revisited. Journal of Automated Reasoning 18(3), 297–336 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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. Düntsch, I., Orłowska, E.: A proof system for contact relation algebras. Journal of Philosophical Logic 29, 241–262 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  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. 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. 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. Knaster, B.: Un theoreme sur les fonctions d’ensembles. Ann. Soc. Polon. Math. 6, 133–134 (1928)

    MATH  Google Scholar 

  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. Lifschitz, V.: Computing circumscription. In: Proc. 9th IJCAI, pp. 229–235. Morgan Kaufmann, San Francisco (1985)

    Google Scholar 

  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. 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)

    Article  MathSciNet  MATH  Google Scholar 

  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. 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. 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. Orłowska, E.: Dynamic logic with program specifications and its relational proof system. Journal of Applied Non-Classical Logic 3, 147–171 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  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. Orłowska, E.: Relational proof systems for relevant logics. Journal of Symbolic Logic 57, 1425–1440 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  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. 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. 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. Orłowska, E., McCaull, W.: A calculus of typed relations. In: [3], pp. 152–158 (2004)

    Google Scholar 

  29. Orłowska, E., Szałas, A. (eds.): Relational Methods for Computer Science Applications. Springer, Heidelberg (2001)

    MATH  Google Scholar 

  30. Simmons, H.: The monotonous elimination of predicate variables. Journal of Logic and Computation 4, 23–68 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  31. Szałas, A.: On the correspondence between modal and classical logic: An automated approach. Journal of Logic and Computation 3, 605–620 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  35. Tarski, A.: A Lattice-theoretical Fixpoint Theorem and its Applications. Pacific Journal of Mathematics 5(2), 285–309 (1965)

    Article  MathSciNet  MATH  Google Scholar 

  36. van Benthem, J.: Modal Logic and Classical Logic. Bibliopolis, Naples (1983)

    Google Scholar 

  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)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. National Institute of Telecommunications, Warsaw, Poland

    Ewa Orłowska

  2. The University of Economics and Computer Science, Olsztyn, Poland

    Andrzej Szałas

  3. Department of Information and Computer Science, University of Linköping, Sweden

    Andrzej Szałas

Authors
  1. Ewa Orłowska
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrzej Szałas
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Mathematics, Statistics and Computer Science, St. Francis Xavier University, Antigonish, NS, Canada

    Wendy MacCaull

  2. Department of Computer Science, Brock University, L2S 3A1, St. Catharines, Ontario, Canada

    Michael Winter

  3. Computer Science Department, Brock University, L2S 3A1, St. Catharines, Ontario, Canada

    Ivo Düntsch

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Orłowska, E., Szałas, A. (2006). Quantifier Elimination in Elementary Set Theory. In: MacCaull, W., Winter, M., Düntsch, I. (eds) Relational Methods in Computer Science. RelMiCS 2005. Lecture Notes in Computer Science, vol 3929. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11734673_19

Download citation

  • DOI: https://doi.org/10.1007/11734673_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-33339-5

  • Online ISBN: 978-3-540-33340-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation