Document Open Access Logo

Conservative Extensions in Guarded and Two-Variable Fragments

Authors Jean Christoph Jung, Carsten Lutz, Mauricio Martel, Thomas Schneider, Frank Wolter

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2017.108.pdf
  • Filesize: 0.57 MB
  • 14 pages

Document Identifiers

Author Details

Jean Christoph Jung
Carsten Lutz
Mauricio Martel
Thomas Schneider
Frank Wolter

Cite AsGet BibTex

Jean Christoph Jung, Carsten Lutz, Mauricio Martel, Thomas Schneider, and Frank Wolter. Conservative Extensions in Guarded and Two-Variable Fragments. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 108:1-108:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.ICALP.2017.108

Abstract

We investigate the decidability and computational complexity of (deductive) conservative extensions in fragments of first-order logic (FO), with a focus on the two-variable fragment FO2 and the guarded fragment GF. We prove that conservative extensions are undecidable in any FO fragment that contains FO2 or GF (even the three-variable fragment thereof), and that they are decidable and 2ExpTime-complete in the intersection GF2 of FO2 and GF.
Keywords
  • Conservative Extensions
  • Decidable Fragments of First-Order Logic
  • Computational Complexity}

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Hajnal Andréka, István Németi, and Johan van Benthem. Modal languages and bounded fragments of predicate logic. J. Philosophical Logic, 27(3):217-274, 1998. Google Scholar
  2. Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, and Peter F. Patel-Schneider, editors. The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, 2003. (2nd edition, 2007). Google Scholar
  3. Vince Bárány, Georg Gottlob, and Martin Otto. Querying the guarded fragment. Logical Methods in Computer Science, 10(2), 2014. Google Scholar
  4. Vince Bárány, Balder ten Cate, and Luc Segoufin. Guarded negation. J. ACM, 62(3):22:1-22:26, 2015. Google Scholar
  5. Michael Benedikt, Balder ten Cate, and Michael Vanden Boom. Interpolation with decidable fixpoint logics. In Proc. of LICS, pages 378-389. IEEE Computer Society, 2015. Google Scholar
  6. Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997. Google Scholar
  7. Elena Botoeva, Boris Konev, Carsten Lutz, Vladislav Ryzhikov, Frank Wolter, and Michael Zakharyaschev. Inseparability and conservative extensions of description logic ontologies: A survey. In Proc. of Reasoning Web, volume 9885 of LNCS, pages 27-89. Springer, 2016. Google Scholar
  8. Stephen D. Comer. Classes without the amalgamation property. Pacific Journal of Mathematics, 28:309-318, 1969. Google Scholar
  9. Bernardo Cuenca Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler. Modular reuse of ontologies: Theory and practice. Journal of Artificial Intelligence Research (JAIR), 31:273-318, 2008. Google Scholar
  10. Giovanna D'Agostino and Marco Hollenberg. Logical questions concerning the μ-calculus: Interpolation, Lyndon and ł oś-Tarski. J. Symb. Log., 65(1):310-332, 2000. Google Scholar
  11. Giovanna D'Agostino and Giacomo Lenzi. Bisimulation quantifiers and uniform interpolation for guarded first order logic. Theor. Comput. Sci., 563:75-85, 2015. Google Scholar
  12. Răzvan Diaconescu, Joseph A. Goguen, and Petros Stefaneas. Logical support for modularisation. In Gerard Huet and Gordon Plotkin, editors, Logical Environments, pages 83-130, 1993. Google Scholar
  13. Silvio Ghilardi, Carsten Lutz, and Frank Wolter. Did I damage my ontology? A case for conservative extensions in description logic. In Proc. of KR, pages 187-197. AAAI Press, 2006. Google Scholar
  14. Valentin Goranko and Martin Otto. Model theory of modal logic. In Patrick Blackburn, Johan van Benthem, and Frank Wolter, editors, Handbook of Modal Logic, pages 249-330. Elsevier, 2006. Google Scholar
  15. Michael J. C. Gordon and Thomas F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993. Google Scholar
  16. Erich Grädel. On the restraining power of guards. J. Symb. Log., 64(4):1719-1742, 1999. Google Scholar
  17. Erich Grädel, Phokion G. Kolaitis, and Moshe Y. Vardi. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic, 3(1):53-69, 1997. Google Scholar
  18. Erich Grädel and Martin Otto. The freedoms of (guarded) bisimulation. In Alexandru Baltag and Sonja Smets, editors, Johan van Benthem on Logic and Information Dynamics, pages 3-31. Springer, 2014. Google Scholar
  19. Erich Grädel, Martin Otto, and Eric Rosen. Two-variable logic with counting is decidable. In Proc. of LICS, pages 306-317. IEEE Computer Society, 1997. Google Scholar
  20. Erich Grädel and Igor Walukiewicz. Guarded fixed point logic. In Proc. of LICS, pages 45-54. IEEE Computer Society, 1999. Google Scholar
  21. Eva Hoogland and Maarten Marx. Interpolation and definability in guarded fragments. Studia Logica, 70(3):373-409, 2002. Google Scholar
  22. Emanuel Kieronski. On the complexity of the two-variable guarded fragment with transitive guards. Inf. Comput., 204(11):1663-1703, 2006. Google Scholar
  23. Emanuel Kieronski, Jakub Michaliszyn, Ian Pratt-Hartmann, and Lidia Tendera. Two-variable first-order logic with equivalence closure. SIAM J. Comput., 43(3):1012-1063, 2014. Google Scholar
  24. Boris Konev, Carsten Lutz, Dirk Walther, and Frank Wolter. Formal properties of modularisation. In Heiner Stuckenschmidt, Christine Parent, and Stefano Spaccapietra, editors, Modular Ontologies: Concepts, Theories and Techniques for Knowledge Modularization, volume 5445 of LNCS, pages 25-66. Springer, 2009. Google Scholar
  25. Boris Konev, Carsten Lutz, Dirk Walther, and Frank Wolter. Model-theoretic inseparability and modularity of description logic ontologies. Artificial Intelligence, 203:66-103, 2013. Google Scholar
  26. Carsten Lutz, Dirk Walther, and Frank Wolter. Conservative extensions in expressive description logics. In IJCAI, pages 453-458, 2007. Google Scholar
  27. Carsten Lutz and Frank Wolter. Foundations for uniform interpolation and forgetting in expressive description logics. In Proc. of IJCAI, pages 989-995. IJCAI/AAAI, 2011. Google Scholar
  28. Johannes Marti, Fatemeh Seifan, and Yde Venema. Uniform interpolation for coalgebraic fixpoint logic. In CALCO, volume 35 of LIPIcs, pages 238-252. Schloss Dagstuhl, 2015. Google Scholar
  29. Michael Mortimer. On languages with two variables. Math. Log. Q., 21(1):135-140, 1975. Google Scholar
  30. Andrew M. Pitts. On an interpretation of second-order quantification in first-order intuitionistic propositional logic. J. of Symbolic Logic, 57, 1992. Google Scholar
  31. Stephen Pollard. Philosophical Introduction to Set Theory. University of Notre Dame Press, 1990. Google Scholar
  32. Ian Pratt-Hartmann. Complexity of the guarded two-variable fragment with counting quantifiers. J. Log. Comput., 17(1):133-155, 2007. Google Scholar
  33. Ian Pratt-Hartmann. Data-complexity of the two-variable fragment with counting quantifiers. Inf. Comput., 207(8):867-888, 2009. Google Scholar
  34. Dana Scott. A decision method for validity of sentences in two variables. Journal of Symbolic Logic, 27:1962, 1962. Google Scholar
  35. Stephen G. Simpson. Subsystems of Second Order Arithmetic. Cambridge University Press, 2009. Google Scholar
  36. Albert Visser. Uniform interpolation and layered bisimulation. In Gödel'96 (Brno, 1996), volume 6 of Lecture Notes in Logic, pages 139-164. Springer, 1996. Google Scholar
  37. Thomas Wilke. Alternating tree automata, parity games, and modal μ-calculus. Bulletin of the Belgian Mathematical Society, 8(2), 2001. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact