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:


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

contradiction

what does X mean?


Contradiction

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

addition: do not add formulae to closed branches

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

follow rules of expansion


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:

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:

in this example, four branches

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:


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:

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