Related papers: Interpolation in First-Order Logic
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…
In this article, a model-theoretic approach is proposed to prove that the first-order G\"odel logic, $\mathbf{G}$, as well as its extension $\mathbf{G}^\Delta$ associated with first-order relational languages enjoy the Craig interpolation…
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…
We develop foundations for computing Craig-Lyndon interpolants of two given formulas with first-order theorem provers that construct clausal tableaux. Provers that can be understood in this way include efficient machine-oriented systems…
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…
Craig interpolation and uniform interpolation have many applications in knowledge representation, including explainability, forgetting, modularization and reuse, and even learning. At the same time, many relevant knowledge representation…
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 surveys some of the main results on interpolation in several of the most prominent families of non-classical logics. Special attention is given to the distinction between the two most commonly studied variants of…
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…
This paper develops a general methodology to connect propositional and first-order interpolation. In fact, the existence of suitable skolemizations and of Herbrand expansions together with a propositional interpolant suffice to construct a…
We develop foundations for computing Craig interpolants and similar intermediates of two given formulas with first-order theorem provers that construct clausal tableaux. Provers that can be understood in this way include efficient…
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…
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…
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 show a projective Beth definability theorem for logic programs under the stable model semantics: For given programs $P$ and $Q$ and vocabulary $V$ (set of predicates) the existence of a program $R$ in $V$ such that $P \cup R$ and $P \cup…
In this paper, we establish an analogue of Craig Interpolation Property for a many-sorted variant of first-order hybrid logic. We develop a forcing technique that dynamically adds new constants to the underlying signature in a way that…
Using a recently introduced algebraic framework for the classification of fragments of first-order logic, we study the complexity of the satisfiability problem for several ordered fragments of first-order logic, which are obtained from the…
We show that the guarded-negation fragment is, in a precise sense, the smallest extension of the guarded fragment with Craig interpolation. In contrast, we show that full first-order logic is the smallest extension of both the two-variable…
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…