2005-04-07
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 ;)
|
echo earlZstrainYat|tr ZY @.
|