method for establishing the satisfiability of a formula
definition of satisfiability:
formula F is satisfiable if there exist M and s such that M,s ⊧ F
a formula only is given
try to build a model M where F is satisfied in one of its worlds
from examples we infer facts about modal logic
is □x ∧ □¬x satisfiable?
proceed by intuition:
formula has to be true in a world s of a model M:
both □x and □¬x have to be true in that world:
in all successors of the state both x and ¬x are true:
contradiction?
looks unsatisfiable, but...
□x ∧ □¬x is satisfiable
just do not create any successor of s:
formula is satisfiable in a model comprising a single world
(regardless of the value of x in that world)
fact 1: do not create successors if not needed
rationale:
note: in some logics, creating a successor may be necessary
(e.g., logics with seriality)
try to find a model for □x ∧ ◇¬x
□x ∧ ◇¬x is satisfiable if there exists a model and a world s where it is true:
since □x ∧ ◇¬x is true in s,
both □x and ◇¬x are true in s |
□x means: x true in all successors
by not creating successors, we avoid a constraint x on them
but ◇¬x is only true if the state has a successor where x is false
if ◇¬x is true in s
s has a successor t where ¬x is true |
since □x is true in s
x is true in all successors of t in this case, x is true in t |
formula is unsatisfiable
fact 2: formulae ◇F impose the creation of successors where F is true
fact 3: once a successor is created, formulae □F act on it by creating a constraint F there
rationale:
example: □x ∧ ◇y ∧ ◇¬y
formula has to be true in a world s:
conjunction: all subformulae have to be true in the same world |
for the moment, disregard boxed formulae
concentrate on diamonds ◇y implies the existence of a successor t where y is true |
◇¬y requires a successor where ¬y is true
try reusing the existing successor t |
look inconsistent
but…
◇¬y requires a successor where ¬y is true
not necessarily the same one create a new successor instead |
left to do: □x makes x true in both t and q
no inconsistency
fact 4: if possible, create different successors for different diamond formulae
notes:
we only consider modal logic K
(no constraint on the accessibility relation)
method:
(x∧¬x)∨(□y∧◇¬y)
try to use the rules for propositional tableau as much as possible
□y∧◇¬y has ∧ as the main connective
can still be expanded using the propositional rules
what now?
rely on intuition for now
◇¬y means: ¬y true in a successor
formalization will be done later
a successor of the initial state exists
□y implies that y is true there
y cannot both true and false in the same state
close branch
requires:
points 2 and 3 explained on examples
formula ◇x ∧ ◇¬x
tableau, informally:
by fact 4, the two successors are better be different
formalization has to include a way for specifying that formulae hold in different worlds
formula ◇¬x ∧ □◇x ∧ □□¬x
as usual: from ◇¬x to ¬x in a successor
the first boxed formula applies to the successor
◇x holds in the successor
a successor of it exists, and x holds in it
from box to the successor, again
box applies
contradiction: x and ¬x in the successor of the successor
the method has to keep track of where formula holds
also of the link between worlds
three methods (in this course)
differ on how they represent worlds and their relations
rationale:
if F is the formula to check for satisfiability:
(i1,…,im) □F |
(i1,…,im,im+1) F |
if (i1,…,im,im+1) is a sequence that is already in the tableau
(i1,…,im) ◇F |
(i1,…,im,im+1) F |
where im+1 is such that (i1,…,im,im+1) is a sequence that is not in the tableau yet
{ □x ∧ ◇y, ◇(¬x ∨ ¬y) }
as usual, tableaux work on sets of formulae
expand ∧
expand first ◇
why (1,1)?
from (1) to (1,i) with i such that (1,i) is not already in the tableau
expand second ◇
from (1) to (1,i)
but (1,1) already taken, use (1,2)
expand □ to (1,1)
note: can be done because (1,1) already exists
expand □ to (1,2)
note: can be done because (1,2) already exists
expand ∨ in (1,1)
note: from formula in (1,1) to formulae in (1,1)
(1,1) x and (1,1) ¬x contradict each other
(only because the world is the same: (1,1))
close branch
note: (1,2)y and (1,1)¬y not contradictory
no other expansion possible
set is satisfiable
model?
consider the unclosed branch
take only literals
result: (1,1) x |
(1,1) x
(1,1) ¬y (1,2) x (1,2) y |
(seq) F means that F holds in world (seq) relation between worlds: (1,1) is a successor of (1) same for (1,2) |
{ □x, □(¬x∨□¬y), ◇(¬x∨◇y) }
principles:
if F is the formula to check for satisfiability:
w/□F wRw' |
w'/F |
preconditions are a labeled formula w/□F and a pseudoformula wRw'
w/◇F |
w'/F wRw' |
where w' is a new symbol
(a symbol not yet in the tableau)
generates a labeled formula w'/F and a pseudoformula wRw'
{ □x, ◇¬x ∨ ◇x }
begin with given formulae
apply usual rule for disjunction
label of new formulae is the same
a diamond formula generates a formula and a pseudoformula
a box formula generates a new formula only in conjuction with an appropriate pseudoformula
formulae are opposite to each other and the world is the same
close branch
other branch: expand diamond
other branch: expand box
no further expansion possible
set is satisfiable
model?
consider open branch
root ⟶ (sat)
take literals and pseudoformulae
w''/x, w''/x, wRw''
w''/x, w''/x, wRw''
model:
very different from previous ones
no labels
each node of the tree contains all formulae true in a world
propositional rules: |
|
|
modal rule: |
|
principle: all box formulae and one diamond formula affect the successor
more than one diamond formula?
in the second case, a search in the space of tableau is needed
still in the "and" sense: satisfiable if no tableau can be closed
{ z∨x, ¬z∧□x, □y, ◇z, ◇(¬x∨¬y) }
first step: all formulae on the first node
expand conjunction
break ¬z∧□x in two
expand disjuction z∨x
two children: both contain all other formulae
first leaf has z and ¬z: close
expand diamonds
two children: each expand all boxes and one diamond
"and" branching: satisfiability is to be proved in both successors
no expansion possible on first child
expand disjunction on second one
both children contain a contraction
open branch: formula satisfiable?
open leaf is on one way of an "and" branching
other way closes (all sub-branches close)
set unsatisfiable