Logikbasierte Wissensrepr¨asentation und Inferenz - Methoden Wissensbasierter Systeme - page 59

∀ x Politiker(x) ⇒ ( ∀ y Knauserig(y) ⇒¬ Mag(x,y))

(1)

∀ x Politiker(x) ⇒∃ y Firma(y) ∧ Mag(x,y)

(2)

x Politiker(x)
Daraus konnen wir folgende Formeln ableiten, wobei wir rechts angeben, auf welche
Formeln welche Inferenzregel (vgl. Abschnitt 3.3.3) angewandt wurde:

(3) ∃

3, ∃ -Inst

(4) Politiker(NN)

Politiker(NN) ⇒∃ y Firma(y) ∧ Mag(NN,y) 2, ∀ -Inst

(5)

∃ y Firma(y) ∧ Mag(NN,y)

(6) 4,5, MP

Firma(AG) ∧ Mag(NN,AG) 6, ∃ -Inst (7)

7, ∧ -Elim

(8) Firma(AG)

(9) Mag(NN,AG) 7, ∧ -Elim

(10) Politiker(NN) ⇒

( ∀ y Knauserig(y) ⇒¬ Mag(NN,y)) 1, ∀ -Inst

∀ ⇒¬

(11) y Knauserig(y) Mag(NN,y) 4,10, MP

⇒¬ ∀

(12) Knauserig(AG) Mag(NN,AG) 11, -Inst

¬ Knauserig(AG)

(13) 9,12, MT

(14) Firma(AG) ∧¬ Knauserig(AG) 8,13, ∧ -Einf

Beachten Sie die Anwendungen der Instantiierungsregeln. In (4) wurde die neue
Konstante NN eingesetzt. Da wir fur (5) wegen der -Instantiierung beliebige zulassi-

ge Terme einsetzen konnen, konnen wir insbesondere auch die Konstante NN einset-
zen. Entsprechend wurde sowohl fur (7) als auch fur (12) die Konstante AG gewahlt.
Die abgeleitete Formel (14) besagt, dass das mit AG bezeichnete Objekt eine Firma
ist, die nicht knauserig ist. Damit ist noch nicht gesagt, welche bestimmte Firma
dies sein mag; nur die Existenz einer solchen Firma haben wir mit der Ableitung
bewiesen.

∀

Bei Ableitungen in PL1 sind in der Praxis, wie auch schon bei der Aussagenlogik
gesagt, nicht nur die Inferenzregeln, sondern auch die entsprechenden Aquivalenzen
von Bedeutung. So haben wir im obigen Beispiel fur die Herleitung der Formel (13)
mittels modus tollens implizit von der

Aquivalenz

¬¬ Mag ( NN , AG ) ≡

Mag ( NN , AG )

Gebrauch gemacht.
Ein entscheidender Aspekt bei einer Ableitung wie in Beispiel 3.62 ist, dass diese
vollstandig mechanisch ablaufen kann. Jede Schlussfolgerung folgt aus den Voraus-
setzungen und den vorangegangenen Schlussfolgerungen aufgrund einer rein syntak-
tisch definierten Anwendung einer Inferenzregel. Naturlich gibt es neben den im Bei-
spiel gewahlten Ableitungsschritten noch eine große Anzahl von anderen moglichen
Ableitungsschritten. Das Finden von Strategien zur intelligenten Auswahl dieser
Schritte, um (moglichst schnell) am Ziel anzugelangen, ist eines der Hauptprobleme
bei der Realisierung automatischer Beweissysteme (vgl. z.B. [17, 19]).