sawind

User info:

Registered: Mar 2008
Posts: 4 (0.00 al dì)
Location: mi
Corso: informatica per le telecomunicaz
Anno: 1
Time Online: 1:21:21 [...]
Status: Offline

Post actions:

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..