Event Detail

The Craig interpolation theorem, proved by William Craig in the 1950s, states that every valid first-order implication A |= B has an interpolant C such that A |= C and C |= B and all non-logical symbols occurring in C occur both in A and in B. Moreover, such an interpolant C can be effectively constructed from a proof of the implication A |= B.

The Craig interpolation theorem is considered one of the cornerstones in our understanding of first-order model theory and proof theory.

Over the last few years, we have seen the emergence of several new applications of Craig interpolation in the area of data management. In particular, interpolation-based techniques have been proposed for querying under access restrictions and semantic query optimization.

These applications, in turn, have led to the study of new variants of Craig interpolation. I will present two such new theorems, namely an interpolation theorem for first-order formulas with relational access restrictions, and an effective interpolation theorem for the guarded-negation fragment of first-order logic.