Confused about how to use semantic tableau to answer questions of satisfiability

Question

I'm taking a course in Mathematical Logic right now and we have to use semantic tableau to find out if a formula is satisfiable (some interpretations give a value of T).

My question is:

Given these examples for logical formulas A and B:

How do I determine how to build the tree? I know that the first time you decompose the formula you remove the conjunction, like this:

       A
p ∧ (¬q ∨ ¬p)
       ↓
  p, ¬q ∨ ¬p

But I'm not sure why this

p, ¬q ∨ ¬p
  /     \
p, ¬q    p, ¬p

happens.

For this part:

Why did this decomposition happen? Can someone explain to me how the tree came to be, step by step? I read the textbook (Ben-Ari Mathematical Logic for Computer Science) and I'm still confused at how to build the tree.

edit: Thank you all for the helpful answers!

Answer 1

See Mordechai Ben-Ari, Mathematical Logic for Computer Science (3rd ed - 2012), page 33 :

The method of semantic tableaux is an efficient decision procedure for satisfiability (and by duality validity) in propositional logic.

The principle behind semantic tableaux is very simple: search for a model (satisfying interpretation) by decomposing the formula into sets of atoms [e.g. propositional letters : $p,q,\ldots$] and negations of atoms. It is easy to check if there is an interpretation for each set: a set of atoms and negations of atoms is satisfiable iff the set does not contain an atom $p$ and its negation $¬p$. The formula is satisfiable iff one of these sets is satisfiable.

For each formula, every step is uniquely defined, because you have to decompose the formula according to the principal connective.

See page 33 :

A literal is an atom or the negation of an atom. An atom is a positive literal and the negation of an atom is a negative literal. For any atom $p, \{ p,¬p \}$ is a complementary pair of literals.

Let :

$$A = p ∧ (¬q ∨¬p).$$

• The principal operator of $A$ is conjunction, so [by truth-tables for connectives; see page 16] $v_I (A) = T$ if and only if both $v_I (p) = T$ and $v_I (¬q ∨¬p) = T$.

• The principal operator of $¬q ∨¬p$ is disjunction, so $v_I (¬q ∨¬p) = T$ if and only if either $v_I (¬q) = T$ or $v_I (¬p) = T$.

Thus we have to apply the procedure to $A$ with the goal of verifying if the formuala $A$ is satisfiable or not.

The procedure will always end, because a formula is a finite string of symbols, with only a finite number of occurrences of connectives.

At every step we decompose the final a formula of a branch according to the principal connective applying the above rules.

If the formula $B$ has as principal connective the conjunction, it is $B_1 \land B_2$. Thus, according to the rules for evaluating the connectives, in order to satisfy $B$ we have that both $B_1$ and $B_2$ must be true. Thus, we add a new node to the branch with both $B_1$ and $B_2$.

If the formula $B$ has as principal connective the disjunction, it is $B_1 \lor B_2$. Thus, according to the rules for evaluating the connectives, in order to satisfy $B$ we have that at least one of $B_1$ and $B_2$ must be true. Thus, we branch, one for each possibility.

---

Part A

Thus, for :

$p ∧ (¬q ∨ ¬p)$

you can only apply the rule for $\land$, because it is the princupal connective.

In the second step :

$p, ¬q ∨ ¬p$

$p$ is atomic, i.e. indecomposable. Thus you can only decompose $¬q ∨ ¬p$, applying the rule for $\lor$.

---

Part B

You have two formulae; thus you can choose how to start.

First decompose $\lnot p \land \lnot q$ and then $p \lor q$, with the branching.

Thus, the "strategy" is : if you can (as in B) use the "branching" rules at the end, in order to have more "compact" trees.

Answer 2

I checked the book, and I think the construction of the semantic tableaux is quite well explained, but I will try to give you some hints about the procedure.

The objective is find a model, an interpretation (a truth assignment to the atoms $p, q$,...) that satisfies the formula. You place the formula at the root (top node) of the tree, and you decompose it, step by step starting from the main operator (connective). At each step (node), depending on the form of the formula that you are decomposing, the tree splits (the node has two child nodes) or not (see Table 2.8 of the book). You follow the procedure until you only have atoms ($p, q$,...) or negations of atoms ($\lnot p, \lnot q$,...) at the bottom (leaves) of the tree. Then you check all the leaves of the tree: if any of them does not contain an atom and its negation, the set of atoms of that leave and all subformulas in the path to the top node are satisfiable.

Let's take example A.

• The main operator is $\land$. For the formula to be T, both subformulas $p$ and $\lnot q \lor \lnot p$ must be true, just one possibility, so that the tree does not split and you write both subformulas separated by a comma in the next node.

• In this node, the first subformula is already an atom ($p$), so nothing to do with it, it will pass unchanged to the next node(s). The other $\lnot q \lor \lnot p$ is a disjuction (main operator $\lor$), so that for it to be T, either $\lnot q$ is T or $\lnot p$ is true. This means that there are two possibilities to satisfy the formula, so that the tree must split: in one node we write $\lnot q$ and the other $\lnot p$ (in both cases with the atom $p$ which as I said passes unchanged)

• Now we have reached the leaves, since we only have atoms or negation or atoms. We have two sets, one for each leave: $\{p,\lnot q\}$ and $\{p,\lnot p\}$. If any of them is satisfiable, the original formula (and all subformulas in the path to the top along that branch of the tree) are also satisfiable. Obviously, $\{p,\lnot p\}$ is not satisfiable, since both $p$ and its negation cannot be T simultaneously, so this path (branch) closes, and we mark it with an X at the bottom. But $\{p,\lnot q\}$ is satisfiable in the interpretation that assigns T to $p$ and F to $q$, so we have found an interpretation that satisfies the formula.

I hope this helps. I am sure that you will be able to do example B.

I just want to add something. I have been talking about truth values, meaning of the logical connectives,... that is about the semantics of the propositional logic, in order to guide you in the process. But the rules for construction of the semantic tableaux can be given (and that is their main objective) as an algorithm in which the rule to apply at each node of the tree only depends on the form (syntaxis) of the formula there, see section 2.6.2 and algorithm 2.64 in the book. In other words, it is a proof system which you (or a computer) can apply to find out if a formula is satisfiable (or valid, or and inference valid, ... all semantic notions) based only on the form (how it is made up of symbols, a syntactic notion) of the formula.