Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Interpolation in Classical Propositional Logic

Patrick Koopmann, Christoph Wernhard, Frank Wolter

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.

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.

Paper Structure

This paper contains 17 sections, 22 theorems, 20 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Craig Interpolants
  4. Uniform Interpolants
  5. Beth Definability
  6. Generalisations and an Application to Theory Decomposition
  7. Interpolants via Quantifier Elimination
  8. Interpolants via DNF
  9. Interpolants via Resolution
  10. Uniform Interpolation Using Resolution
  11. Craig Interpolation Using Resolution
  12. Bibliographic and Historic Remarks
  13. Craig Interpolants via Analytic Tableaux
  14. A Tableau Proof System
  15. Craig-Lyndon Separator Extraction from a Closed Tableau
  16. ...and 2 more sections

Key Result

Theorem 2

In propositional logic, if $\varphi\models \psi$, then there exists a Craig interpolant for $\varphi,\psi$.

Figures (1)

  • Figure 1: A more complex example of Craig-Lyndon separator extraction, discussed in Example \ref{['examp-tab-separator-complex']}.

Theorems & Definitions (43)

  • Definition 1: Craig Interpolant
  • Theorem 2: Craig Interpolation Property (CIP)
  • Example 3
  • Theorem 4: Closure of Craig Interpolants under Conjunction and Disjunction
  • Definition 5: Craig Separator
  • Definition 6: Craig-Lyndon Interpolant
  • Example 7
  • Theorem 8: Craig-Lyndon Interpolation Property (LIP)
  • Definition 9: Craig-Lyndon Separator
  • Definition 10: Uniform Interpolant
  • ...and 33 more