3 papers
cs.LO2026
Craig-Lyndon Interpolation for the Logic of Here and There with a Variation of Mints' Sequent System
Christoph Wernhard
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 , a su…
cs.LO2025
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…
cs.LO2025
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…