SAT for a formula using Tableaux Propositional Logic (precedence of operators)

Question

My doubt is in check if the following formula $\phi$ is SAT or not using the Tableaux Method. Let me write formula:

$\phi = \neg \left ( p \vee q \supset \left ( \left ( \neg p \wedge q \right ) \vee p \vee \neg q \right ) \right )$

How start rules of tableaux method in this case?

Answer 1

You have to apply the rule corresponding to the principal connective of the negated formula.

Assuming the usual convention for omitting parentheses, we have that conjunction and disjunction symbols apply to as little as possible.

Thus, the formula will be read as :

$¬[(p∨q) \to ((¬p∧q)∨p∨¬q)]$.

In this case, the formula is the negation of a conditional; thus, you have to start using the rule :

$\lnot (\alpha \to \beta)$.

Answer 2

Thank you! I apply the rest of Tableaux Method if can be useful for someone.

$p \vee q$ $[\mu_1]$from rule of AND. I apply tableaux method for this point later..

$ \neg ( (\neg p \wedge q) \vee p \vee \neg q)$ from rule of AND, associative property

$ \neg (\neg p \wedge q) \wedge \neg(p \vee \neg q)$ de Morgan property

$\neg (\neg p \wedge q) $ rule of AND

$\neg(p \vee \neg q)$ rule of OR

$p \vee \neg q $ $[\mu_2]$

$\neg p \wedge q $

$\neg p$

$q$

..apply first OR $[\mu_1]$

$\beta_1$ branch: $p$ clash! Branch closed.

$\beta_2$ branch: $q$

..apply second OR $[\mu_2]$

$\beta_{2_1}$ branch: $p$ clash! Branch closed.

$\beta_{2_2}$ branch: $\neg q$ clash! Branch closed.

We can say that $\phi$ is UNSAT.