Let
and
. Show that using TC1 that
(a)
is valid, and
(b)
is not a logical consequence of
a)
---
aufgelöst
---
aufgelöst durch neue Skolem Konstante a und
aufgelöst durch neue Skolem Konstante b
---
aufgelöst durch neue Skolem Konstante b und
aufgelöst durch neue Skolem Konstante a
--- clash in branch
is valid
b)
iff
is unsatisfiable. (Siehe pl1.pdf Folie 48)
---
aufgelöst
---
und
aufgelöst durch ground term a
---
aufgelöst durch neue Skolem Konstante b,
aufgelöst durch neue Skolem Konstante c
--- no clash deshalb
ist statisfiable, bedeutet
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)