TU Wien:Einführung in wissensbasierte Systeme VU (Egly)/Übungen WS12/Blatt 3 - Beispiel 1

Let $T$ be a theory consisting of the formulas

$T=\left\lbrace {\begin{aligned}\forall x(p(x)\lor r(x)),\\\forall x(\neg q(x)\rightarrow r(x)),\\p(a)\land r(b),\\\neg q(a)\end{aligned}}\right\rbrace$

over the alphabet containing unary predicate symbols $p$, $q$, and $r$, and only the object constants $a$ and $b$.

1. Which of the literals $p(b)$, $q(b)$, $r(b)$, $\neg p(b)$, $\neg q(b)$ and $\neg r(b)$ are contained in ${\text{CWA}}(T)$?
2. ${\text{CWA}}(T)$ consistent? Justify your answer.
3. Are the following formulas contained in ${\text{CWA}}(T)$?
   1. $p(a)\land p(b)$
   2. $\exists x(p(x)\land r(x))$
   3. $\neg q(a)\rightarrow r(a)$

Theorie

CWA

Closed-world assumption (CWA) of theory T

${\begin{aligned}T_{asm}&=\{\lnot P\mid P\,\,{\text{ground atom}},\,T\nvDash P\}\\{\text{CWA}}(T)&=\{\varphi \mid T\cup T_{asm}\models \varphi ,\varphi \,{\text{closed}}\}=Cn(T\cup T_{asm})\end{aligned}}$

CWA consistency

CWA consistency theorem

Let $T\,$ be a consistent theory. Then:

${\text{CWA}}(T)\,$ is inconsistent iff there are ground atoms $A_{1},...,A_{n}\,$ such that

$T\models A_{1}\lor ...\lor A_{n}\,$

but $T\nvDash A_{i}\,$, for all $i=1,...,n\,$.

Lösungsvorschlag 3dm45t3r

$T=\{\forall x(p(x)\lor r(x))$,(1.1)

$\forall x(\lnot q(x)\rightarrow r(x))$,(1.2)

$p(a)\land r(b)$,(1.3)

$\lnot q(a)\}$(1.4)

CWA

Annahmen müssen für folgende ground atome getroffen werden: $p(a),p(b),q(b),r(a),r(b)$

$T\models p(a)$ durch die Inferenz Regel Simplification von 1.3 oder TC herleitbar

$T\nvDash p(b)$

$T\nvDash q(b)$

$T\models r(a)$ durch TC herleitbar

$T\models r(b)$ durch die Inferenz Regel Simplification von 1.3 oder TC herleitbar

$T_{asm}=\{\lnot p(b),\lnot q(b)\}$

$CWA(T)=Cn(T\cup T_{asm})=$

$Cn(\{\forall x(p(x)\lor r(x)),\forall x(\lnot q(x)\rightarrow r(x)),p(a)\land r(b),\lnot q(a),\lnot p(b),\lnot q(b)\})$

---

a) Which of the literals $p(b),q(b),r(b),\lnot p(b),\lnot q(b)$ and $\lnot r(b)$ are contained in $CWA(T)$?

$p(b)\notin CWA(T)$

$q(b)\notin CWA(T)$

$r(b)\in CWA(T)$

$\lnot p(b)\in CWA(T)$

$\lnot q(b)\in CWA(T)$

$\lnot r(b)\notin CWA(T)$

---

b) Is $CWA(T)$ consistent?

Ja da $T\models p(a)\lor \lnot q(a)\lor r(b)$ jedoch $T\models p(a)$

$T\models \lnot q(a)$ und $T\models r(b)$

---

c)Are the following formulas contained in $CWA(T)$?

• (1.5)$p(a)\land p(b)\notin CWA(T)$ da $p(a),\lnot p(b)\in CWA(T)$

• (1.6)$\exists x(p(x)\land r(x))\in CWA(T)$

• (1.7)$\lnot q(a)\rightarrow r(a)\in CWA(T)$

Kommentar Terminal

Habe ich genauso

mir ist nicht ganz klar, wie/wo ihr euch $r(a)$ ableitet. so weit ich das seh, gilt $T\nvDash r(a)$ --Thrau (Diskussion) 19:20, 6. Dez. 2012 (CET)

Wenn du dir die Formel 1.2 ansiehst ist mit x=a die implikation nur erfüllt wenn r(a) erfüllt ist (hoffe das sind die richtigen adjektive ;-) ) --Trambampolin (Diskussion) 13:05, 7. Dez. 2012 (CET)

$\forall x(\lnot q(x)\rightarrow r(x))\equiv \forall x(q(x)\lor r(x))$. ich kann über T kein tableau auflösen in dem $r(a)$ gilt. bitte beweisen ;-) --Thrau (Diskussion) 15:18, 7. Dez. 2012 (CET)

r(a) kann man aus 1.2 zusammen mit 1.4 herleiten --3dm45t3r

ah ja, jetzt seh ich's. keine ahnung was ich da rumgetan hab. --Thrau (Diskussion) 18:38, 10. Dez. 2012 (CET)