The Triguarded Fragment of First-Order Logic

Sebastian RudolphSebastian Rudolph, Mantas SimkusMantas Simkus

Sebastian Rudolph, Mantas Simkus
The Triguarded Fragment of First-Order Logic
In Gilles Barthe, Geoff Sutcliffe, Margus Veanes, eds., Proceedings of the 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 57 of EPiC Series in Computing, 604-619, 2018. EasyChair

Details
Bibtex

KurzfassungAbstract
Past research into decidable fragments of first-order logic (FO) has produced two very prominent fragments: the guarded fragment GF, and the two-variable fragment FO2. These fragments are of crucial importance because they provide significant insights into decidabil- ity and expressiveness of other (computational) logics like Modal Logics (MLs) and various Description Logics (DLs), which play a central role in Verification, Knowledge Represen- tation, and other areas. In this paper, we take a closer look at GF and FO2, and present a new fragment that subsumes them both. This fragment, called the triguarded fragment (denoted TGF), is obtained by relaxing the standard definition of GF: quantification is required to be guarded only for subformulae with three or more free variables. We show that, in the absence of equality, satisfiability in TGF is N2ExpTime-complete, but becomes NExpTime-complete if we bound the arity of predicates by a constant (a natural assumption in the context of MLs and DLs). Finally, we observe that many natural extensions of TGF, including the addition of equality, lead to undecidability.
Weitere Informationen unter:Further Information: Link
Projekt:Project: DeciGUT
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@inproceedings{RS2018,
  author    = {Sebastian Rudolph and Mantas Simkus},
  title     = {The Triguarded Fragment of First-Order Logic},
  editor    = {Gilles Barthe and Geoff Sutcliffe and Margus Veanes},
  booktitle = {Proceedings of the 22nd International Conference on Logic for
               Programming, Artificial Intelligence and Reasoning},
  series    = {EPiC Series in Computing},
  volume    = {57},
  publisher = {EasyChair},
  year      = {2018},
  pages     = {604-619},
  doi       = {https://doi.org/10.29007/m8ts}
}