Primer 3

Proveriti da li je formula F=(p*(p->q))->q valjana (tautologija).

F je tautologija ako je –F nezadovoljiva.

Prvo ćemo da predstavimo –F u KNF

-( (p*(p->q))->q )

A->B = -A + B                     -( -(p*(p->q)) + q )

A->B = -A + B                     -( -(p*(-p + q)) + q )

-(A+B) = -A * -B                 -( -(p*(-p + q)) ) * ( -q )

--A = -A                               (p*(-p + q))  * ( -q )

--A = -A                               (p*(-p + q))  * ( -q )

Sredimo zagrade i eto ga KNF: (p) * (-p + q)  * (-q)   a odgovarajući D={ {p},{-p,q},{-q} }

DPLL(D):

(unit propagation) D[p->1]            (1) * (-1 + q)  * (-q)                           D={ {1},{-1,q},{-q} }

(zamena negacije literala)            (1) * (0 + q) * (-q)                             D={ {1},{0,q},{-q} }

(uklanjanje 0 literala)                    (1) * (q) * (-q)                                   D={ {1},{q},{-q} }

(tautology)                                    (q) * (-q)                                           D={ {q},{-q} }

(unit propagation) D[q->1]           (1) * (-1)                                            D={ {1},{-1} }

(zamena negacije literala)           (1) * (0)                                             D={ {1},{0} }

(uklanjanje 0 literala)                   (1) * ()                                               D={ {1}, { ø } }

(sadrži praznu klauzu)                return NE

-F nije zadovoljiva (ne postoji interpretacija u kojoj je –F tačna) što znači da F mora biti tačna u svim interpretacijama, odnosno da je F tautologija-valjana formula.