Constructive interpolation for guarded logics

The guarded fragment of first-order logic (GFO) shares many useful properties with modal logic, but fails to have Craig interpolation. Recently, an extension called the guarded negation fragment (GNFO) was shown to have interpolation, but the proof was non-constructive. The goal in this research (suggested by Benedikt, ten Cate, and Lutz) is to develop constructive methods for interpolation, in order to see whether interpolation can be performed in practice and to better understand the complexity of the problem. I describe some preliminary work on constructive interpolation for GNFO.

Authors

• Michael Vanden Boom

Keywords

No keywords are indexed for this paper.