Metodo dei Tableux

Si utilizza una struttura ad albero dove ogni nodo si dirama in 1 o 2 archi. Iniziamo inserendo la formula da verificare nella radice dell’albero e andremo a scomporla fino ad ottenere una contraddizione o una formula atomica, quindi non più scomponibile.

Se incontriamo contraddizioni in tutti i nodi la formula è insoddisfacibile Se vogliamo verificare una tautologia infatti possiamo negarla e verificare che ci siano solo contraddizioni.

Possiamo dividere le formule in più regole, congiuntive e disgiuntive

Regole alfa $α_{1}$ : $x \land y$ diventa $x, y$ $α_{2} : \neg (x \lor y) d i v e n t a \neg x, \neg y$ $α_{3} : \neg (x \to y) d i v e n t a x, \neg y$ $α_{4} : x \leftrightarrow y d i v e n t a x \leftrightarrow y, y \leftrightarrow x$ $α_{5} : \neg\neg x d i v e n t a x$

Regole beta $β_{1} : x \lor y l o se p er iam o in x y$ $β_{2} : \neg (x \land y) l o se p a r iam o in \neg x \neg y$ $β_{3} : x \to y l o se p a r iam o in \neg x y$ $β_{4} : \neg (x \leftrightarrow y) l o se p a r iam o in \neg (x \to y) \neg (y \to x)$

Regole Tableux Predicativi $\forall x A x$ diventa $\forall x A x, A a$ $\neg\exists x B x$ diventa $\neg\exists x B x, \neg B a$ $\exists x A x$ diventa $A a$ $\neg\forall x B x$ diventa $\neg B a$

👨🏻‍💻 Alem's Notes

Metodo dei Tableux

Esercizi di esempio

Backlinks