Compito esame ragionamento automatico
Primo appello 2007

Domanda 1

Verificare la soddisfacibilità della seguente formula usando la procedura Davis-Putnam (DPLL). In particolare, mostrare l'albero di ricerca, evidenziando in ogni nodo i letterali che si ottengono per propagazione unitaria e uso dei letterali puri.

{ a &or b, ¬ a &or c, ¬ a &or d, a ∨ ¬ b ∨ c ∨ d, ¬ b ∨ ¬ c ∨ ¬ d, a ∨ c ∨ ¬ d, ¬ c ∨ d, ¬ a ∨ c ∨ e ∨ f, ¬ a ∨ b &or ¬ e ∨ ¬ f }

Domanda 2

Verificare la soddisfacibilità della seguente formula usando il metodo tableaux. Usare a scelta il metodo con o senza unificazione.

{ ∃ x ∀ y Q(x, y), &forall x ¬ Q(a, x), ∀ x (Q(a, x) ∨ ¬ Q(x, x)) }

Domanda 3

Mostrare i vari passi che vengono effettuati per forzare la consistenza di arco (arc consistency) sul seguente problema. Ad ogni passo, dire su quale archi e nodi si effettua la propagazione e dire quali valori vengono eliminati.

variabili
{x, y, z, w}
domini
vincoli