.dsy:it. - esercizio compitino..

.dsy:it.
//www.dsy.it

esercizio compitino..

Posted by sawind on 04-04-2008 18:15

Ragazzi, qualcuno di voi..saprebbe dirmi dove e se ho sbagliato qualcosa..??
Verifica tautologia..
(p1---->q1)^(p2---->q2)---->(p1Vp2 ---->q1^q2)
¬((p1---->q1)^(p2---->q2)---->(p1Vp2 ---->q1^q2))
((p1---->q1)^(p2---->q2)^¬(p1Vp2 ---->q1^q2)
(¬p1Vq1)^(¬p2Vq2)^((p1Vp2)^¬(q1^q2))
(¬p1Vq1)^(¬p2Vq2)^(p1Vp2)^(¬q1V¬q2)

DPLL
{¬p1Vq1,¬p2Vq2,p1Vp2,¬q1V¬q2}
Applicando lo split su p1 e successivamente unit resolution e subsumption
{q1,¬p2Vq2,¬q1V¬q2}
Applicando poi la assert su q1 e poi la unit resolution
{¬p2Vq2,¬q2}
Assert su q2 e poi unit resolution
{¬p2}

p1=1,q1=1,q2=0,p2=0
dato che ¬A è soddisfacibile nn è una tautologia.

Può essere una cosa del genere..??grazie..