Forum by laureateci.it - Chiarimento Tableaux

Nome Utente:	Password:
Salva Password
Password Dimenticata?

Tutti i Forum

Magistrale - Primo Anno

Metodi formali dell'Informatica

Chiarimento Tableaux

Nuova Discussione

Rispondi

Versione Stampabile

Aggiungi Segnalibro

Autore

Discussione

WonderBoy
Utente giovane

Città: UK

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.

Ivan86
Utente Capoeirista

Regione: Puglia
Prov.: Bari
Città: Bitritto

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

WonderBoy
Utente giovane

Città: UK

Inserito il - 10/11/2009 : 10:13:57

Ok grazie mille...

Discussione

Nuova Discussione

Rispondi

Versione Stampabile

Aggiungi Segnalibro

Vai a:

Forum by laureateci.it

Il DB ha risposto in 0,13 secondi.