From the 1 of 4 linked papers with an AI index.
4 papers
Craig-Lyndon Interpolation for the Logic of Here and There with a Variation of Mints' Sequent System
Christoph Wernhard
The paper introduces a two‑stage method for constructing Craig‑Lyndon interpolants in the three‑valued propositional logic of Here‑and‑There (HT) by adapting Maehara’s interpolatio…
Interpolation in Classical Propositional Logic
Patrick Koopmann, Christoph Wernhard, Frank Wolter
We introduce Craig interpolation and related notions such as uniform interpolation, Beth definability, and theory decomposition in classical propositional logic. We present four ap…
Interpolation with Automated First-Order Reasoning
Christoph Wernhard
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 inte…
Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic
Jan Heuer, Christoph Wernhard
We show a projective Beth definability theorem for logic programs under the stable model semantics: For given programs and and vocabulary (set of predicates) the existe…