Musterlösung zu Aufgabe 3.11

Aus Semantic-Web-Grundlagen

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