Interpolation in Classical Propositional Logic

Patrick Koopmann; Christoph Wernhard; Frank Wolter

doi:10.48550/arXiv.2508.11449

Interpolation in Classical Propositional Logic

Patrick Koopmann
, Christoph Wernhard^*
, Frank Wolter

^*Corresponding author for this work

Research output: Working paper / Preprint › Preprint › Professional

Abstract

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 elimination, from formulas in disjunctive normal form, and by extraction from resolution or tableau refutations. We close with a discussion of the size of interpolants and links to circuit complexity.

Original language	English
DOIs	https://doi.org/10.48550/arXiv.2508.11449
Publication status	Published - 15 Aug 2025

Access to Document

10.48550/arXiv.2508.11449

Persistent URL (handle)

Persistent link

Cite this

@techreport{46692e89b361424887aabf630b0358cd,

title = "Interpolation in Classical Propositional Logic",

abstract = "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 elimination, from formulas in disjunctive normal form, and by extraction from resolution or tableau refutations. We close with a discussion of the size of interpolants and links to circuit complexity.",

author = "Patrick Koopmann and Christoph Wernhard and Frank Wolter",

year = "2025",

month = aug,

day = "15",

doi = "10.48550/arXiv.2508.11449",

language = "English",

type = "WorkingPaper",

}

TY - UNPB

T1 - Interpolation in Classical Propositional Logic

AU - Koopmann, Patrick

AU - Wernhard, Christoph

AU - Wolter, Frank

PY - 2025/8/15

Y1 - 2025/8/15

N2 - 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 elimination, from formulas in disjunctive normal form, and by extraction from resolution or tableau refutations. We close with a discussion of the size of interpolants and links to circuit complexity.

AB - 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 elimination, from formulas in disjunctive normal form, and by extraction from resolution or tableau refutations. We close with a discussion of the size of interpolants and links to circuit complexity.

U2 - 10.48550/arXiv.2508.11449

DO - 10.48550/arXiv.2508.11449

M3 - Preprint

BT - Interpolation in Classical Propositional Logic

ER -

Interpolation in Classical Propositional Logic

Abstract

Access to Document

Persistent URL (handle)

Fingerprint

Cite this