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)

to prove the unsatisfiability of the set

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

first place the formulae in column:

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

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

still a conjunction: place formulae below the other ones:

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?

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*

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*

*a* and *¬ a* in the same branch

contradiction

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)

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)

*b* and *¬b* in the same branch

(branch from *a ∧ c* to *¬b*)

close branch

*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?

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**

- 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

addition: do not add formulae to closed branches

logics different from propositional logic require other 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)

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

first step: place formulae in a line

follow rules of expansion

all branches close ⇒ set is unsatisfiable

what if some branches do not close?

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

expand every formula once

enough?

every formula has been expanded at least once

tableau not closed

yet, set is unsatisfiable

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?

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*

general rule:

in every branch, every formula has to be expanded once

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

expand every formula in every branch

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}*

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

*B*_{1}=A ∧ B ∧ C ∧ E ∧ H*B*_{2}=A ∧ B ∧ C ∧ E ∧ I*B*_{3}=A ∧ B ∧ D ∧ F*B*_{4}=A ∧ B ∧ D ∧ G ∧ J

semantics of the tableau is
*B _{1} ∨ B_{3} ∨ B_{3} ∨ B_{4}*

let *D=K ∨ L*, expand it on *J*

⇒ |

the semantics changes: the last branch is made two

⇒ |

old semantics:
*B _{1} ∨ B_{3} ∨ B_{3} ∨ B_{4}*

*B _{4}* is replaced by two new formulae:

*B*_{4}=*A ∧ B ∧ D ∧ G ∧ J**B'*_{4}=*A ∧ B ∧ D ∧ G ∧ J ∧ K = B*_{4}∧ K*B''*_{4}=*A ∧ B ∧ D ∧ G ∧ J ∧ L = B*_{4}∧ L

new semantics:
*B _{1} ∨ B_{2} ∨ B_{3} ∨ B'_{4} ∨ B''_{4}*

equivalent to:
*B _{1} ∨ B_{2} ∨ B_{3} ∨ (B_{4} ∧ K) ∨ (B_{4} ∧ L)*

equivalent to:
*B _{1} ∨ B_{2} ∨ B_{3} ∨
(B_{4} ∧ ( K ∨ L))*

since *B _{4}* contains

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

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

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

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 | disjunctions first |

expanding disjunctions creates new branches

conjunctions may need to be expanded in all of them

better expand conjunctions first

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

the method of tableaux is a system for *refutation*

it can prove that a set is unsatisfiable

we can use it to prove entailment:

Aif and only if_{1},..., A_{n}⇒ B{Ais unsatisfiable_{1},..., A_{n}, ¬B}