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

Spiegazione DPLL

Qualche anima buona mi può spiegare come funziona la procedura di DPLL? Trasformo la formula in fnn, poi in fnc (e fin lì ok), poi prendo l'insieme delle clausole, che sarà nella forma C0={C1,C2,C3,...}, e applico le 9 regole.... ma come? Grazie mille a chiunque vorrà aiutarmi.

EDIT: rifacendo gli esercizi passo per passo ho più o meno capito i passaggi, però faccio fatica a "finire" l'esercizio, ad es. quando ho {p=1, q=1} |- {not q} come devo procedere? Non ho ben capito le regole di asserzione e del letterale puro...