Craig-Interpolation

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

Die Craig-Interpolation ist ein Ausdruck der Logik. Der zugrunde liegende Satz (Craig’s Lemma, Interpolationstheorem) lautet folgendermaßen:

Es seien und zwei Theorien und der Satz sei ein in ableitbarer Satz. Dann gilt: Es gibt ein , sodass in ableitbar ist, und ist in ableitbar.

Das Interpolationstheorem[Bearbeiten | Quelltext bearbeiten]

Dieses Interpolationstheorem wurde zuerst von dem US-amerikanischen Logiker William Craig (1918–2016) 1953 aufgestellt. Es wurde von S. Maehara und von Kurt Schütte (für intuitionistische Kalküle) bewiesen und hat zahlreiche Anwendungen in der Beweis- und Modelltheorie.

Algorithmus zur Bestimmung der Craig-Interpolante[Bearbeiten | Quelltext bearbeiten]

Voraussetzung: Die Formel sei ableitbar.

  1. Suche alle Atome, die in , aber nicht in enthalten sind.
  2. Für jedes dieser Atome ver-odere (Verknüpfung mit oder) mit sich selbst, wobei jedes dieser Atome einmal mit und einmal mit belegt werden muss.
  3. Die resultierende Formel ist die Craig-Interpolante .

Literatur[Bearbeiten | Quelltext bearbeiten]