ABSTRACT. We complete Maksimova's classification of the normal extensions of S4 with interpolation. In particular, we prove Craig interpolation for the six extensions of S4 for which Craig interpolation was still open. The proof strategy builds upon the ideas of Smoryński, but employs a novel approach using Fine's frame formulas for splitting clusters.

ABSTRACT. We present a variation of Maehara's method to construct Craig-Lyndon interpolants for the three-valued propositional logic of here and there (HT), also known as Gödel's G₃, a superintuitionistic logic of importance in logic programming. Our method adapts a recent interpolation technique that operates on classically encoded logic programs to a variation of Mints' sequent system for HT. The approach is characterized by two stages: First, a preliminary interpolant is constructed, a formula that is an interpolant in some sense but not yet the desired HT formula. In the second stage, an actual HT interpolant is obtained from this preliminary interpolant. With the classical encoding, the preliminary interpolant is a classical Craig-Lyndon interpolant for classical encodings of the two input HT formulas. In the presented adaptation, the sequent system operates directly on HT formulas, and the preliminary interpolant is in a nonclassical logic that generalizes HT by an additional logic operator.

ABSTRACT. In this paper we focus on the intersection of two important results: Russellian theory of definite descriptions (RDD) and Craig interpolation theorem (CIT). RDD provides the most recognisable approach to formalisation of complex terms. CIT is one of the most important metalogical results hence it is crucial to show that it holds for a theory like RDD. One of the possible ways of proof-theoretic characterisation of RDD was provided by means of a cut-free sequent calculus satisfying the subformula property. In the paper we apply this system to obtain a Maehara-style constructive proof of CIT for RDD.

ABSTRACT. We establish the Lyndon interpolation property for basic lattice expansion logics (LE-logics) in arbitrary signatures using display calculi. Our approach is {\em constructive}, yielding interpolants algorithmically from derivations, and {\em modular}, in the sense that interpolation for axiomatic extensions can be obtained by verifying a local interpolation property for the analytic structural rules corresponding to the additional axioms. To this end, we identify a class of \emph{interpolation-safe} structural rules preserving local Lyndon interpolation. As applications of the general framework, we show that the tense version of Holliday's fundamental modal logic enjoys the Lyndon interpolation property.

ABSTRACT. Recent research has established complexity results for the problem of deciding the existence of interpolants in logics lacking the Craig interpolation property (CIP). The proof techniques developed so far are non-constructive, and no meaningful bounds on the size of interpolants are known. Hybrid modal logics (or modal logics with nominals) are a particularly interesting class of logics without CIP: in their case, CIP cannot be restored without sacrificing decidability and, in applications, interpolants in these logics can serve as definite descriptions and separators between positive and negative data examples in description logic knowledge bases. In this contribution we show, using a new hypermosaic elimination technique, that in many standard hybrid modal logics Craig interpolants can be computed in fourfold exponential time, if they exist. On the other hand, we show that the existence of uniform interpolants is undecidable, which is in stark contrast to modal or intuitionistic logic where uniform interpolants always exist.

ABSTRACT. Propositional formulas frequently contain implicitly defined variables, and extracting their explicit definitions is often useful. Following the standard proof of Beth's definability theorem, these definitions can be obtained as Craig interpolants of formulas expressing implicit definability. In practice, one calls a SAT solver for each defined variable and extracts an interpolant from the resulting resolution proof. We propose an alternative approach where a single resolution refutation serves as a witness of definability for a set of variables. We then present a simple modification of standard interpolation systems that constructs a multi-output circuit representing all definitions in one pass over this proof. The running time and circuit size are $O(nm)$, where $n$ is the number of defined variables and $m$ the proof size. Preliminary experiments on Boolean functional synthesis benchmarks show that the single refutation witnessing definability is produced at least as quickly as the sequence of proofs of a per-variable baseline, but that the multi-output circuits are typically larger, sometimes substantially so on instances with many definitions. Extraction that asymptotically improves upon $O(nm)$ is identified as the main open question.