Interpolation for Guarded Logics

Given a valid implication in the guarded negation fragment of first-order logic, there is an interpolant that also lives in the guarded negation fragment. However, the model-theoretic methods originally used to prove this result were non-constructive. I will present recent work exploring constructive methods for interpolation in guarded logics. One theme is the exploitation of the tree-like model property for these logics, which enables us to use tools from modal logic and automata theory.

Authors

• Michael Vanden Boom

Keywords

No keywords are indexed for this paper.