.dsy:it. (http://www.dsy.it/forum/)
- Logica matematica (http://www.dsy.it/forum/forumdisplay.php?forumid=246)
-- Aiuto DPLL (http://www.dsy.it/forum/showthread.php?threadid=34491)

----- Primo esercizio di Simeon -----

p=1,r=0 - {s,¬s} (qui non mi convinceva la sparizione di t e l'applicazione del letterale puro)

qui c'e' r e non c'e' ¬r, per cui applico il letterale puro (e' giusto?)

r=1 - {pvq,¬q V ¬s V p, ¬p V ¬s}

spezzo su p

[RAMO p=1]

p=1 - {s,¬s} (q sparisce... boh=

Mah, l'ho fatto senza nessuna ragione particolare, volendo avrei potuto prendere prima s e farci l'asserzione, ma poi mi rimaneva la clausola vuota tra le palle e l'ho lasciata per ultima

Se il procedimento e' giusto penso vada bene uguale.

All'inizio non si puo applicare nulla quindi applico lo spezzamento su p. Perchè sul secondo ramo non compare p=0 ma q=0.

Sicuro che è corretto?

__________________
?

si poi mi sono accorto... grazie

solo un dubbio, ma se vedo che il primo ramo di uno spezzamento è soddisfacibile non è finito l'esercizio?

in questo caso nel 2) si puo applicare nuovamente il letterale puro e dimostare che è sodisfacibile, senza usare lo spezzamento, o sbaglio?


r=1,s=0 - {pvq}
E fare lo spezzamento qui.

solo un dubbio, ma se vedo che il primo ramo di uno spezzamento è soddisfacibile non è finito l'esercizio?

__________________
?

Originally posted by yeah


Dal momento che avevi (not) r e r=0, ti rimaneva t per risoluzione unitaria (regola 2.3); a parte quel passaggio, il risultato è giusto per quel ramo.

Giusto, ah nel passaggio subito è comparso (not) r anziché (not) s, sicuramente un errore di battitura, lo scrivo per altri che potrebbero leggerlo

Non è formalmente sbagliato, però lo spezzamento è meglio tenerlo come ultima spiaggia, e applicare prima tutte le altre, se si può. Dal momento che avevi (not) s e non avevi s, potevi applicare il letterale puro ottenendo:
r=1,s=0 - {pvq,¬q V ¬s V p, ¬p V ¬s}
r=1,s=0 - {pvq}
E fare lo spezzamento qui.

Dal momento che le regole possono essere applicate in modo sparso, si possono ottenere percorsi diversi, ciò che conta è il risultato finale, che deve essere uguale.

q non "sparisce", ma si trova in una clausola in cui compare anche p e poiché a p hai assegnato 1, la clausola in cui compare q è soddisfatta qualsiasi sia il valore di verità che le assegneresti (dal momento che è in OR con p).

=1,s=0 - {pvq}
E fare lo spezzamento qui.

una cosa sul es. 2 dopo aver arrivato a:

r = 1, s = 0 - {p V q} applico il letterale puro su p ed ottengo:

r = 1, s = 0, p = 1 che la rende soddisfacibile.

ma q?? il suo vale è indifferente??

stessa cosa avviene se invece di p prendo q.

__________________
by Ð@rk§h@ÐØw

se ti rimane p V q assegni a p il valore 1. per il letterale puro a questo punto riscrivi p V q e il passaggio successivo cancelli l'intera clausola perchè se hai p V q e p è vera allora di conseguenza lo è anche q.

detto in termini logici.

r = 1, s = 0 - {p V q} applico il letterale puro su p ed ottengo:

r = 1, s = 0, p = 1 - {p v q} applico quindi una sussunzione ed ho:

r = 1, s = 0, p = 1 - zero quindi sat

ciao

per quanto riguarda la teoria?? c'e' nel compito??

per esempio in un compito c'e' questo esercizio:

Sia A V B una contraddizione e sia r una lettera proposizionale. Allora
1) il sequente A ----> r è dimostrabile
2) il sequente r ----> A è dimostrabile
3) il sequente r ----> A V B è dimostrabile

come si fa??

__________________
by Ð@rk§h@ÐØw

Originally posted by darkshadow
per quanto riguarda la teoria?? c'e' nel compito??

per esempio in un compito c'e' questo esercizio:

Sia A V B una contraddizione e sia r una lettera proposizionale. Allora
1) il sequente A ----> r è dimostrabile
2) il sequente r ----> A è dimostrabile
3) il sequente r ----> A V B è dimostrabile

come si fa??

Originally posted by Simeon
Dimostrabile ? Cos'e' quella roba ? :o

Magari hai guardato a compiti PARECCHIO vecchi.

__________________
by Ð@rk§h@ÐØw

Eh no scusa, se ho r=0 su ¬r si usa la sussunzione, per cui sparisce l'intera clausola ¬r V t. O no?

E quindi e' giusto ? Se poi mi scrivi "il resto e' corretto" non capisco

Perche' spezzamento? abbiamo p e non abbiamo ¬p, abbiamo q e non abbiamo ¬q, non si puo' semplicemente applicare il letterale puro a uno dei due? Lo spezzamento si fa quando non si puo' fare altro no?

ma q?? il suo vale è indifferente??

__________________
?

Originally posted by darkshadow
No. è il tema d'esame di giugno 2006.

Di nulla.
Auguri per l'esame

__________________
?

Salve a tutti, avrei bisogno di una mano sempre riguardo DPLL. Quello che non riesco a comprendere è quali regole utilizzare, questo perchè non riesco a "tradurre" la notazione. Per esempio nella sussunzione, nel caso di I(p)=1 si ha:
I |- C U (p V C)
____________
I |- C

dove C rappresenta l'insieme delle clausole C.
Quello che non capisco è cosa intende per (pVC), come riconosco in un insieme di clausole se mi trovo in questa situazione?
Grazie

p V altra roba: se p è vero, nell'or il risultato finale è in ogni caso vero, e puoi cancellare tutta la clausola.

Originally posted by michele.c
p V altra roba: se p è vero, nell'or il risultato finale è in ogni caso vero, e puoi cancellare tutta la clausola.