Craig Interpolation and Access Interpolation with Clausal First-Order Tableaux

We develop foundations for computing Craig
interpolants and similar intermediates of two given formulas
with first-order theorem provers that construct clausal
tableaux.  The framework of clausal tableaux emerged in the
1990s from relating three directions of research: fully
automated first-order theorem proving, tableaux methods,
which are targeted more at interactive theorem proving and
verification, also in non-classical logics, and model
generation with "bottom-up" methods.  Provers that can be
understood in terms of this framework include efficient
machine-oriented systems based on calculi of two families:
goal-oriented like model elimination and the connection
method, and bottom-up like the hyper tableau calculus.  The
presented method for Craig-Lyndon interpolation involves a
lifting step where terms are replaced by quantified
variables, similar as known for resolution-based
interpolation, but applied to a differently characterized
ground formula and proven correct on a more abstract basis.
Access interpolation is a recent form of interpolation for
database query reformulation that applies to first-order
formulas with relativized quantifiers and constrains the
quantification patterns of predicate occurrences.  It has
been previously investigated in the framework of
"non-clausal" analytic tableaux.  Here, in essence, we
simulate these with the more machine-oriented clausal
tableaux through structural constraints that can be ensured
either directly by bottom-up tableau construction methods
or, for closed clausal tableaux constructed with arbitrary
calculi, by postprocessing with restructuring
transformations.