Musterlösung zu Aufgabe 3.11

Aus Semantic-Web-Grundlagen

Version vom 09:14, 8. Okt. 2011 bei Sebastian Rudolph (Diskussion | Beiträge)

(Unterschied) ← Nächstältere Version | Aktuelle Version (Unterschied) | Nächstjüngere Version → (Unterschied)

1. Schritt: Instanziierung von $\neg H \sqcup \exists r.H$ :

$\neg H \sqcup \exists r.H (t)$

2. Schritt: $\sqcup$ -Regel anwenden:

erster Tableauzweig enthält $\neg H (t)$ anderer Tableauzweig enthält $\exists r.H (t)$

Schon der erste Taleauzweig hat die Eigenschaft, dass keine Tableauregel mehr angewendet werden kann, die zu etwas Neuem führen würde. Damit ist haben wir einen nicht abgeschlossenen, nicht erweiterbaren Tableauzweig gefunden, folglich ist die Wissensbasis erfüllbar.

Musterlösung zu Aufgabe 3.11

Aus Semantic-Web-Grundlagen

Persönliche Werkzeuge

Navigation

Suche

Ansichten

Werkzeuge