Related papers: Interpolation in Non-Classical Logics
We prove that there are continuum-many axiomatic extensions of the full Lambek calculus with exchange that have the deductive interpolation property. Further, we extend this result to both classical and intuitionistic linear logic as well…
In this chapter we give a basic overview of known results regarding Craig interpolation for first-order logic as well as for fragments of first-order logic. Our aim is to provide an entry point into the literature on interpolation theorems…
Interpolation is an important property of classical and many non classical logics that has been shown to have interesting applications in computer science and AI. Here we study the Interpolation Property for the propositional version of the…
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 provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path…
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…
Craig's interpolation theorem (Craig 1957) is an important theorem known for propositional logic and first-order logic. It says that if a logical formula $\beta$ logically follows from a formula $\alpha$, then there is a formula $\gamma$,…
We introduce Craig interpolation and related notions such as uniform interpolation, Beth definability, and theory decomposition in classical propositional logic. We present four approaches to computing interpolants: via quantifier…
Interpolation is an important property of classical and many non-classical logics that has been shown to have interesting applications in computer science and AI. Here we study the Interpolation Property for the the non-monotonic system of…
Traditionally, research on Craig interpolation is concerned with (a) establishing the Craig interpolation property (CIP) of a logic saying that every valid implication in the logic has a Craig interpolant and (b) designing algorithms that…
We show that a vast class of finitary fragments of geometric logic admit a form of Craig interpolation property. In doing so, we provide a new dictionary to import technology from algebraic logic to categorical logic.
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…
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…
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…
Normal modal logics extending the logic K4.3 of linear transitive frames are known to lack the Craig interpolation property, except some logics of bounded depth such as S5. We turn this `negative' fact into a research question and pursue a…
There are exactly two maximal schematic extensions of the relevant logic R with the variable sharing property. We establish that one of them has a strong form of interpolation for deducibility, thereby giving an example of a well-known…
This work contributes to the theory of judgment aggregation by discussing a number of significant non-classical logics. After adapting the standard framework of judgment aggregation to cope with non-classical logics, we discuss in…
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…
We consider the family of guarded and unguarded ordered logics, that constitute a recently rediscovered family of decidable fragments of first-order logic (FO), in which the order of quantification of variables coincides with the order in…
This chapter provides a comprehensive overview of proof-theoretic methods for establishing interpolation properties across a range of logics, including classical, intuitionistic, modal, and substructural logics. Central to the discussion…