License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2018.43
URN: urn:nbn:de:0030-drops-99424
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9942/
Go to the corresponding LIPIcs Volume Portal

Padmanabha, Anantha ; Ramanujam, R ; Wang, Yanjing

Bundled Fragments of First-Order Modal Logic: (Un)Decidability

pdf-format:
LIPIcs-FSTTCS-2018-43.pdf (0.6 MB)

Abstract

Quantified modal logic is notorious for being undecidable, with very few known decidable fragments such as the monodic ones. For instance, even the two-variable fragment over unary predicates is undecidable. In this paper, we study a particular fragment, namely the bundled fragment, where a first-order quantifier is always followed by a modality when occurring in the formula, inspired by the proposal of [Yanjing Wang, 2017] in the context of non-standard epistemic logics of know-what, know-how, know-why, and so on.
As always with quantified modal logics, it makes a significant difference whether the domain stays the same across possible worlds. In particular, we show that the predicate logic with the bundle "forall Box" alone is undecidable over constant domain interpretations, even with only monadic predicates, whereas having the "exists Box" bundle instead gives us a decidable logic. On the other hand, over increasing domain interpretations, we get decidability with both "forall Box" and "exists Box" bundles with unrestricted predicates, where we obtain tableau based procedures that run in PSPACE. We further show that the "exists Box" bundle cannot distinguish between constant domain and variable domain interpretations.

BibTeX - Entry

@InProceedings{padmanabha_et_al:LIPIcs:2018:9942,
  author =	{Anantha Padmanabha and R Ramanujam and Yanjing Wang},
  title =	{{Bundled Fragments of First-Order Modal Logic: (Un)Decidability}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software  Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{43:1--43:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Sumit Ganguly and Paritosh Pandya},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9942},
  URN =		{urn:nbn:de:0030-drops-99424},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.43},
  annote =	{Keywords: First-order modal logic, decidability, bundled fragments}
}

Keywords: First-order modal logic, decidability, bundled fragments
Collection: 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)
Issue Date: 2018
Date of publication: 05.12.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI