# Propositional tableaux

method to prove the unsatisfiability of a set of formulae

principle:

break each formula into its components up to the simplest ones, where contradiction is easy to spot

create a tree structure called tableau
(plural: tableaux)

### Propositional tableau: example

to prove the unsatisfiability of the set

{ a ∧ c, (¬a ∨ b) ∧ (¬b ∨ ¬ c) }

first place the formulae in column:

### Example, second step

since we have a ∧ c, place a and c below the other formulae:

### Example, third step

same as before, but for (¬a ∨ b) ∧ (¬b ∨ ¬ c)

still a conjunction: place formulae below the other ones:

### Example, fourth step

we already broke the two conjuctions a ∧ b and (¬a ∨ b) ∧ (¬b ∨ ¬ c) into their components

do the same for the disjunctions

but, for disjunction make two branches

for ¬a ∨ b:

what did we do, so far?

### Meaning of branches

each branch (path from root to a leaf) is a different way to satisfy the formulae in the original set

in this case:

two ways to satisfy the set:

• make true all formulae in the branch a ∧ c ... ¬ a
• make true all formulae in the branch a ∧ c ... b

### Rules of expansion

to satisfy A ∧ B we have to satisfy both A and B

we place both A and B below

to satisfy A ∨ B, we have to satisfy either A or B

two different ways to satisfy the same formula

we make a branch for A and one for B

### Example, fifth step

a and ¬ a in the same branch

what does X mean?

each branch is a way to satisfy the set

a and ¬ a in the same branch

this possibility is not viable

close the branch (mark it with X)

### Example, sixth step

expand ¬b ∨ ¬c

the first branch is closed

we already excluded it as a possible way to satisfy the set

go in the other possibility (the other branch)

### Example, seventh step

b and ¬b in the same branch

(branch from a ∧ c to ¬b)

close branch

### Example, eighth step

c and ¬c in the same branch

note that each branch is a full path from root to a leaf

in this case, from a ∧ c to ¬c

close branch

conclusion?

### Example: conclusion

final tableau:

each branch is a possible way to satisfy the set

closed branch = possibility excluded because of contradiction

all closed = no way to satisfy the set

conclusion: {a ∧ c, (¬a ∨ b) ∧ (¬b ∨ ¬ c)} is unsatisfiable

### Propositional tableau: rules

• place formulae in a line
• expand according to the following rules:
 A ∧ B A B
 A ∨ B A | B
• if a branch contains complementary literals (e.g., x and ¬ x), close the branch

logics different from propositional logic require other rules

### Application of rules

in this situation:

we can apply

 P C

getting:

pretty obvious in this case

not so for tableau for other logics (e.g., first-order logic)

### Another example

{(a ∨ b) ∧ c, ¬b ∨ ¬c, ¬a}

first step: place formulae in a line

### Solution

all branches close ⇒ set is unsatisfiable

what if some branches do not close?

### Open branches: multiple application

{¬a ∨ b, ¬a ∨ ¬b, a ∨ c, ¬ c}

expand every formula once

enough?

### After expanding every formula once

every formula has been expanded at least once

tableau not closed

yet, set is unsatisfiable

### The choice not taken

consider the branch ending in b

each branch is a different way to satisfy the set

the formulae in this branch are: ¬a ∨ b, ¬a ∨ ¬b, a ∨ c, ¬ c, ¬ a, ¬b

for ¬a ∨ b we took ¬ a

for ¬a ∨ ¬b we took ¬ b

no choice have been made for a ∨ c

choose either a or c

in terms of tableaux?

### Multiple applications

in terms of tableaux: expand a ∨ c

principles:

• each branch is a possible way to satisfy the formulae
• for every possibility, break formulae into their smallest components

in the example, there are still unbroken formulae in the branch ending in b

### Multiple application: final tableau

general rule:

in every branch, every formula has to be expanded once

### Open branches: satisfiability

{a ∧ c, a ∨ b, ¬a ∨ ¬b}

expand every formula in every branch

### Satisfiability: final tableau

in the second branch (a ∧ c ... ¬ b) every formula has been expanded once:

a ∧ c
taken both a and c
a ∨ b
chosen a
¬a ∨ ¬b
chosen ¬b

this is a way to satisfy the set that does not lead to contradiction

the set is satisfiable

model: take the literals in the branch

a, c, a, ¬b

model: {a=true, b=false, c=true}

### Semantics of tableau

given a tableau, its semantics is a formula:

• the semantics of a branch is the conjunction of the formulae in the branch
• the semantics of the tableau is the disjunction of the formulae of all its branches

in this example, four branches

• B1=A ∧ B ∧ C ∧ E ∧ H
• B2=A ∧ B ∧ C ∧ E ∧ I
• B3=A ∧ B ∧ D ∧ F
• B4=A ∧ B ∧ D ∧ G ∧ J

semantics of the tableau is B1 ∨ B3 ∨ B3 ∨ B4

### Rules of expansion

let D=K ∨ L, expand it on J ⇒ the semantics changes: the last branch is made two ⇒ ### Semantic change, in formulae

old semantics: B1 ∨ B3 ∨ B3 ∨ B4

B4 is replaced by two new formulae:

B4 =
A ∧ B ∧ D ∧ G ∧ J
B'4 =
A ∧ B ∧ D ∧ G ∧ J ∧ K  =  B4 ∧ K
B''4 =
A ∧ B ∧ D ∧ G ∧ J ∧ L  =  B4 ∧ L

new semantics: B1 ∨ B2 ∨ B3 ∨ B'4 ∨ B''4

equivalent to: B1 ∨ B2 ∨ B3 ∨ (B4 ∧ K) ∨ (B4 ∧ L)

equivalent to: B1 ∨ B2 ∨ B3 ∨ (B4 ∧ ( K ∨ L))

since B4 contains K ∨ L, this is equivalent to the original formula

a similar fact holds for conjunctions: expanding a tableau creates a new one with an equivalent semantics

### How tableaux work

given {A, B, C}, place them in a line

the formula of this tableau is A ∧ B ∧ C

expand formulae, which means:

• creating simpler formulae from complex ones
• still maintaining equivalence with the original set

### Partial models

a tableau for a satisfiable set detects a number of partial models of the formula covering all models of the formula

example: {a ∨ b, ¬b ∨ c}

the three unclosed branches lead to a partial model each:

• {a=true, b=false}
• {a=true, c=true}
• {b=true, c=true}

every model of the set can be obtained by setting the unassigned variable to an arbitrary value in one of these three partial models

### Propositional tableaux: policy

consider again the set {(a ∨ b) ∧ c, ¬b, ∨ ¬c, ¬a}

expanding first conjunctions and then disjunctions, we get:

what happens if we do the opposite? (first disjunctions then conjunctions)

### Conjunctions first vs. disjunctions first  conjunctions first disjunctions first

expanding disjunctions creates new branches

conjunctions may need to be expanded in all of them

better expand conjunctions first

### Effects of wrong policies on semantics

using the wrong policy (e.g., expanding disjunctions first) leads to an increase of size of the table, which leads to an increase of time

yet, unsatisfiability is still proved if set is unsatisfiable

this is not the case for other logics, where applying the wrong policy may inhibit proving unsatisfiability of some unsatisfiable sets

### Refutation and entailment

the method of tableaux is a system for refutation

it can prove that a set is unsatisfiable

we can use it to prove entailment:

A1,..., An ⇒ B if and only if {A1,..., An, ¬B} is unsatisfiable