viernes, 6 de febrero de 2009

Deducción natural

Porque hay varias formas de perder la cabeza.

|- (p -> q) \/ (q -> r) usando LEM

1. q \/ ¬q LEM
2. qpremisa temporal
3. ppremisa temporal
4. qcopy 2
5. p -> q->i(3-4)
6. (p -> q) \/ (q -> r)\/i1(5)
7. ¬qpremisa temporal
8. qpremisa temporal
9. _|_¬e(8,7)
10. r_|_e(9)
11. q -> r->i(8-10)
12. (p -> q) \/ (q -> r)\/i2(11)
13. (p -> q) \/ (q -> r)\/e(1,2-6,7-12)

qed

No hay comentarios: