Eseguire l'algoritmo di Davis-Putnam (DPLL) sul seguente insieme, e dire se è o meno soddisfacibile. Mostrare l'albero di ricerca, evidenziando in ogni nodo i letterali che si ottengono per propagazione unitaria e uso dei letterali puri.
{
a ∨ b,
a ∨ ¬ c,
a ∨ ¬ b ∨ c,
¬ c ∨ ¬ d ∨ e,
d ∨ e,
¬ a ∨ b ∨ ¬ c,
¬ a ∨ ¬ b ∨ ¬ e,
d ∨ ¬ e ∨ ¬ b,
¬ a ∨ b ∨ c,
¬ a ∨ c ∨ e
}
Dimostrare la seguente implicazione usando il metodo della deduzione naturale.
∀ x (¬ P(x) ∨ ¬ Q(x)), ∃ x P(x) ⇒ ¬ ∀ x Q(x)
Suggerimento: assumere il negato della conclusione e cercare di dimostrare ⊥. Possono essere utili le regole di eliminazione di ∃ e ∀ e il modus ponens (da A e A→B si deriva B). Nella deduzione naturale non si usa invece la Skolemizzazione.
Dire se il seguente problema è arc-consistente e se è path-consistente. Nel caso di non-consistenza, dire come va modificato per farlo diventare sia arc-consistente che path-consistente.
|
|
|