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:
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
|
|
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:
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:
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:
in this example, four branches
semantics of the tableau is B1 ∨ B3 ∨ B3 ∨ B4
let D=K ∨ L, expand it on J
⇒ |
the semantics changes: the last branch is made two
⇒ |
old semantics: B1 ∨ B3 ∨ B3 ∨ B4
B4 is replaced by two new formulae:
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
given {A, B, C}, place them in a line
the formula of this tableau is A ∧ B ∧ C
expand formulae, which means:
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
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:
A1,..., An ⇒ B if and only if {A1,..., An, ¬B} is unsatisfiable