Database Reference
In-Depth Information
Diese beiden wichtigsten Eigenschaften einer Ableitungsrelation, Korrektheit und
Vollstandigkeit, konnen also kurz und pragnant durch
|
=gdw.
ausgedruckt werden; manchmal wird dies auch symbolisch durch
|
=
≡
dargestellt.
3.3.5
Logisches Folgern durch Widerspruch
Ein vollstandiger Kalkul muss also alle semantischen Folgerungen ableiten konnen.
Andererseits gilt in vielen Logiken (insbesondere in der Aussagenlogik und in
der Pradikatenlogik 1. Stufe) das Theorem des “Logischen Folgerns durch Wider-
spruch”. Dieses Theorem besagt, dass sich die semantische Folgerbarkeit auf die
Unerfullbarkeit einer Formel(menge) zuruckfuhren lasst.
Theorem 3.21 (Logisches Folgern durch Widerspruch)
Seien
F, G
aussa-
genlogische Formeln oder geschlossene PL1-Formeln. Dann gilt:
•
F
ist allgemeingultig gdw.
¬
Fistunerfullbar.
•
F
|
= G
gdw.
¬
(F
⇒
G)
ist unerfullbar.
•
F
|
= G
gdw.
F
∧¬
G
ist unerfullbar.
Viele Deduktionsverfahren - wie etwa das Resolutionsverfahren, s. Abschnitt 3.6,
- basieren auf diesem Prinzip, eine logische Folgerung auf die Unerfullbarkeit einer
Formel(menge) zuruckzufuhren: Um zu zeigen, dass aus einer gegebenen Formel-
menge F die Formel G logisch folgt (F
= G), wird die zu zeigende Formel G
negiert und zur Ausgangsmenge F hinzugefugt. Ist die resultierende Formel F
|
∧¬
G
unerfullbar, so folgt G logisch aus F .
Es gibt Kalkule, die die Unerfullbarkeit einer Formelmenge durch die Ableitung
eines Widerspruchs zeigen. Ist R nun ein solcher, so genannter
negativer Testkalkul
(wie z.B. der noch zu besprechende Resolutionskalkul),
so soll die Ableitungsre-
lation
R
aus den unerfullbaren Formeln gerade einen elementaren Widerspruch
ableiten. Im Resolutionskalkul wird ein solcher elementarer Widerspruch durch
dargestellt.
Anstatt nun die oben definierte Vollstandigkeit von R zu verlangen, reicht es
aus, dass man mit R aus jeder unerfullbaren Formel einen elementaren Widerspruch
ableiten kann. Diese Eigenschaft wird
Widerlegungsvollstandigkeit
(engl.
refutation
completeness
)genannt.IstR korrekt und widerlegungsvollstandig, so gilt also
F
|= G
gdw.
F ∧¬G
R
