English

Conservative Extensions in Guarded and Two-Variable Fragments

Logic in Computer Science 2017-05-30 v1

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^2 and the guarded fragment GF. We prove that conservative extensions are undecidable in any FO fragment that contains FO2^2 or GF (even the three-variable fragment thereof), and that they are decidable and 2\ExpTime-complete in the intersection GF2^2 of FO2^2 and GF.

Keywords

Cite

@article{arxiv.1705.10115,
  title  = {Conservative Extensions in Guarded and Two-Variable Fragments},
  author = {Jean Christoph Jung and Carsten Lutz and Mauricio Martel and Thomas Schneider and Frank Wolter},
  journal= {arXiv preprint arXiv:1705.10115},
  year   = {2017}
}

Comments

Full version of paper accepted at ICALP 2017