| V I S U A L I Z Z A D I S C U S S I O N E |
| WonderBoy |
Inserito il - 10/11/2009 : 01:42:14
Salve a tutti, in questo esempio di tableaux,
dopo il livello 6) non riesco a capire perchè risale l'albero e verifica P v Q quando è possibile risolvere la formula non atomica
Q --> R.
Inoltre successivamente come mai nei due rami risolve P --> R?
C'è un algoritmo preciso da seguire?
Grazie a tutti. |
| 2 U L T I M E R I S P O S T E (in alto le più recenti) |
| WonderBoy |
Inserito il - 10/11/2009 : 10:13:57
Ok grazie mille... |
| Ivan86 |
Inserito il - 10/11/2009 : 10:02:40
Indico con -R = not R
Viene risolto prima il (2) e si ottiene così (4) e poi -R
Poi risolve il (3) e si ottiene (5) e (6)
A questo punto devi risolvere (4), (5) e (6). Puoi partire da quello che vuoi.
Per semplicità si è fatto P v Q che divide gia in 2 rami. Ora devi risolvere P->R su entrambi i rami.
Infine, viene risolto Q->R |
