start | find | index | login or register | edit
2005-04-07
by earl, 7180 days ago
zur feier des tages ein beweis des einfachen satzes (-p v p) & (q v -q) in GOL+. nicht sonderlich spektakulaer, aber immerhin, dem handgefertigten beweiser und Prolog sei dank:

?- prove((-p v p) & (q v -q)).

1. |- p, -p
-------------------------------------------------- o(1)
2. |- -p v p, -p

3. |- q, -q
-------------------------------------------------- o(3)
4. |- q v-q, q
-------------------------------------------------- o(4)
5. |- q v-q, q v-q
-------------------------------------------------- w(5)
6. |- q v-q, -p
-------------------------------------------------- a(2, 6)
7. |- (-p v p)& (q v-q), -p
-------------------------------------------------- o(7)
8. |- -p v p, (-p v p)& (q v-q)

9. |- p, -p
-------------------------------------------------- o(9)
10. |- -p v p, -p
-------------------------------------------------- o(10)
11. |- -p v p, -p v p
-------------------------------------------------- w(11)
12. |- -p v p, q

13. |- q, -q
-------------------------------------------------- o(13)
14. |- q v-q, q
-------------------------------------------------- a(12, 14)
15. |- (-p v p)& (q v-q), q
-------------------------------------------------- o(15)
16. |- q v-q, (-p v p)& (q v-q)
-------------------------------------------------- a(8, 16)
17. |- (-p v p)& (q v-q), (-p v p)& (q v-q)

spannend? i thought so ;)
powered by vanilla
echo earlZstrainYat|tr ZY @.
earl.strain.at • esa3 • online for 8674 days • c'est un vanilla site