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  T1 und  T2 zwei Theorien und der Satz  A \rightarrow C sei ein in  T1 \cup T2 ableitbarer Satz. Dann gilt: Es gibt ein  B, sodass  A \rightarrow B in  T1 ableitbar ist, und  B \rightarrow C ist in  T2 ableitbar.

Das Interpolationstheorem[Bearbeiten]

Dieses Interpolationstheorem wurde zuerst von dem US-amerikanischen Logiker William Craig (* 1918) 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]

Voraussetzung: Die Formel  A \rightarrow C sei ableitbar.

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

Literatur[Bearbeiten]