Craig-Interpolation
aus Wikipedia, der freien Enzyklopädie
Die Craig-Interpolation ist ein Ausdruck der Logik. Der zugrunde liegende Satz (Craig's Lemma, Interpolationstheorem) lautet folgendermaßen:
Wenn die implikative Formel 
ableitbar ist, dann gibt es eine Interpolante B mit der Eigenschaft, dass auch die Formeln 
und 
ableitbar sind.
[Bearbeiten] Das Interpolationstheorem
Dieses Interpolationstheorem wurde zuerst von dem amerikanischen Logiker W. Craig 1953 aufgestellt. Es wurde von S. Maehara und von K. Schütte (für intuitionistische Kalküle) bewiesen und hat zahlreiche Anwendungen in der Beweis- und Modelltheorie.
[Bearbeiten] Algorithmus zur Bestimmung der Craig-Interpolante
Voraussetzung: Die Formel sei ableitbar.
- Suche alle Atome, die in A, aber nicht in C enthalten sind.
- 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.
- Die resultierende Formel ist die Craig-Interpolante B.
[Bearbeiten] Literatur
- Kurt Schütte: Proof Theory, Berlin Heidelberg New York 1977
