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

Let $\phi =\forall x\exists y.likes(x,y)$ and $\psi =\exists y\forall x.likes(x,y)$. Show that using TC1 that

(a) $\psi \to \phi$ is valid, and

(b) $\psi$ is not a logical consequence of $\phi$

Lösungsvorschlag von 3dm45t3r

a)

$\psi \to \phi \equiv \lnot \psi \lor \phi$

$NNF(\neg (\neg \psi \vee \phi ))=\psi \wedge \neg \phi$

$\psi \land \lnot \phi$

$\exists y\forall x.likes(x,y)\land \lnot (\forall x\exists y.likes(x,y))$

$\exists y\forall x.likes(x,y)\land \exists x\forall y.\lnot likes(x,y)$

--- $\land$ aufgelöst

$\exists y\forall x.likes(x,y)$

$\exists x\forall y.\lnot likes(x,y)$

--- $\exists y$ aufgelöst durch neue Skolem Konstante a und $\exists x$ aufgelöst durch neue Skolem Konstante b

$\forall x.likes(x,a)$

$\forall y.\lnot likes(b,y)$

--- $\forall x$ aufgelöst durch neue Skolem Konstante b und $\forall y$ aufgelöst durch neue Skolem Konstante a

$likes(b,a)$

$\lnot likes(b,a)$

--- clash in branch

$\psi \to \phi$ is valid

---

b)

$\phi \models \psi$ iff $\phi \land \lnot \psi$ is unsatisfiable. (Siehe pl1.pdf Folie 48)

$\forall x\exists y.likes(x,y)\land \lnot (\exists y\forall x.likes(x,y))$

$\forall x\exists y.likes(x,y)\land \forall y\exists x.\lnot likes(x,y)$

--- $\land$ aufgelöst

$\forall x\exists y.likes(x,y)$

$\forall y\exists x.\lnot likes(x,y)$

--- $\forall x$ und $\forall y$ aufgelöst durch ground term a

$\exists y.likes(a,y)$

$\exists x.\lnot likes(x,a)$

--- $\exists y$aufgelöst durch neue Skolem Konstante b, $\exists x$aufgelöst durch neue Skolem Konstante c

$likes(a,b)$

$\lnot likes(c,a)$

--- no clash deshalb $\phi \land \lnot \psi$ ist statisfiable, bedeutet $\phi \not \models \psi$

Lösungsvorschlag von Caranthir

https://web.archive.org/web/*/http://www.logic.at/lvas/til/SS11/til_PL_tab_1in1.pdf

In dieser Folie kann man die Antwort auf b) finden und ein ganz ähnliches Bsp für a)