Related papers: Interpolation in Proof Theory
In this chapter, we present six different proofs of Craig interpolation for the modal logic K, each using a different set of techniques (model-theoretic, proof-theoretic, syntactic, automata-theoretic, using quasi-models, and algebraic). We…
We prove a generalization of Maehara's lemma to show that the extensions of classical and intuitionistic first-order logic with a special type of geometric axioms, called singular geometric axioms, have Craig's interpolation property. As a…
Uniform interpolation is a strengthening of interpolation that holds for certain propositional logics. The starting point of this chapter is a theorem of A. Pitts, which shows that uniform interpolation holds for intuitionistic…
Craig's Interpolation theorem has a wide range of applications, from mathematical logic to computer science. Proof-theoretic techniques for establishing interpolation usually follow a method first introduced by Maehara for the Sequent…
Craig interpolation is a widespread method in verification, with important applications such as Predicate Abstraction, CounterExample Guided Abstraction Refinement and Lazy Abstraction With Interpolants. Most state-of-the-art model checking…
Craig interpolation is a fundamental property of classical and non-classic logics with a plethora of applications from philosophical logic to computer-aided verification. The question of which interpolants can be obtained from an…
This chapter presents a state-of-the-art survey of relationships, traditionally referred to as `bridges', between interpolation properties for propositional logics -- including superintuitionistic, modal, and substructural logics -- and…
In \cite{Craig}, we introduced a syntactically defined and highly general class of calculi known as \emph{semi-analytic}. We then demonstrated that any sufficiently strong (modal) substructural logic with a semi-analytic calculus must…
A modular proof-theoretic framework was recently developed to prove Craig interpolation for normal modal logics based on generalizations of sequent calculi (e.g., nested sequents, hypersequents, and labelled sequents). In this paper, we…
This is a survey on propositional proof complexity aimed at introducing the basics of the field with a particular focus on a method known as feasible interpolation. This method is used to construct "hard theorems" for several proof systems…
Pitts' proof-theoretic technique for uniform interpolation, which generates uniform interpolants from terminating sequent calculi, has only been applied to logics on an intuitionistic basis through single-succedent sequent calculi. We adapt…
We consider interpolation from the viewpoint of fully automated theorem proving in first-order logic as a general core technique for mechanized knowledge processing. For Craig interpolation, our focus is on the two-stage approach, where…
We try to bring to light some combinatorial structure underlying formal proofs in logic. We do this through the study of the Craig Interpolation Theorem which is properly a statement about the structure of formal derivations. We show that…
The two-way modal mu-calculus is the extension of the (standard) one-way mu-calculus with converse (backward-looking) modalities. For this logic we introduce two new sequent-style proof calculi: a non-wellfounded system admitting infinite…
We formalise and mechanise a construtive, proof theoretic proof of Craig's Interpolation Theorem in Isabelle/HOL. We give all the definitions and lemma statements both formally and informally. We also transcribe informally the formal…
Theory interpolation has found several successful applications in model checking. We present a novel method for computing interpolants for ground formulas in the theory of equality. The method produces interpolants from colored congruence…
Craig interpolation is used in program verification for automating key tasks such as the inference of loop invariants and the computation of program abstractions. This chapter covers some of the most important techniques that have been…
Uniform interpolation property (UIP) is a strengthening of Craig interpolation property. It was first established by Pitts(1992) based on a pure proof-theoretic method. UIP in multi-modal $\mathbf{K_n}$, $\mathbf{KD_n}$ and $\mathbf{KT_n}$…
These lecture notes survey the emerging area of Universal Proof Theory, which investigates general questions about the existence, equivalence, and characterization of good proof systems for broad classes of logics. In particular, the notes…
Proof-theoretic methods are developed for subsystems of Johansson's logic obtained by extending the positive fragment of intuitionistic logic with weak negations. These methods are exploited to establish properties of the logical systems.…