Craig Interpolation for Guarded Fragments
Logic in Computer Science
2023-04-18 v1
Abstract
We show that the guarded-negation fragment (GNFO) is, in a precise sense, the smallest extension of the guarded fragment (GFO) with Craig interpolation. In contrast, %we show that the smallest extension of the two-variable fragment (FO2) with Craig interpolation is full first-order logic.
Cite
@article{arxiv.2304.08086,
title = {Craig Interpolation for Guarded Fragments},
author = {Balder ten Cate and Jesse Comer},
journal= {arXiv preprint arXiv:2304.08086},
year = {2023}
}
Comments
Accepted for presentation at DPFO 2023 workshop