the problem with ground tableaux:
there could be a large number, sometimes infinite, of terms t to use in the rule ∀x F/F[t/x]
some or most of these terms may be useless,
sometimes dangerous (increase size of tableau and nothing else)
how to choose t?
the idea is:
do not choose t
apply the rule ∀x F/F[t/x] but leave t unspecified
{∀x P(x), ¬P(f(a))}
preliminary version shown for illustration
actual method: later
only applicable rule is expansion of ∀x P(x)
do not choose a term t, leave it unspecified
(actual method is not like this,
will be shown later)
P( ) is not a valid formula
label for: P(something)
where "something" is to be decided
now?
branch can be closed by choosing f(a) as the term that was unspecified
put f(a) in P( )
branch (and tableau, in this case) can be closed
{∀x P(x), ∃x (¬P(x) ∨ ¬P(f(x)))}
general rule is to expand existential quantifiers first
for the sake of this example, we do the converse
the argument to P is left void
will be chosen later
after expanding the existential quantifier and the disjunction
P( ) is still empty (term to be decided)
what to put in is now clear
by choosing c, we close a branch
choosing f(c) we close the other
we have to decide: P( ) cannot contain both c and f(c)
(only one term!)
as an example, we choose c
tableau after putting c in the third formula
first branch can now be closed
second branch unclosed
expansion of universal quantifier can be still applied to it
tableau after expanding the universal quantifier a second time
if P( ) is filled with f(c), the second branch can be closed
expanding ∀x P(x) first was not the best choice
however, since the result was the partially specified term P( ), it was afterwards possible to fill it with something useful
principles:
problems:
P( ) represents P(t) with t to be decided
in first-order logic, terms and variables represent values of the domain
use a variable as a placeholder
better suited for defining a semantics
expand ∀P(x)
instead of P( ) use a new variable x1 as a placeholder
P(x1) means: P applied to a term that will be chosen later
expanded as usual
x1=c closes first branch
second branch would be closed by x1=f(c)...
... but cannot, because x1 has already been decided to be c
no point in using x1 again to expand ∀x P(x)
(already assigned to c)
new placeholder for a new term; new variable
second branch can be closed by choosing f(c) for x2
next example illustrates a concept about the values chosen for variables
(not just an example)
{ ∀x ¬P(x,a), P(a,b), ∀x∀y (P(x,y) → P(y,x)) }
tableau after some steps
first branch (leaf ¬P(x2,x3)) closes with:
x2=a and x3=b
like using a and b when expanding the universal quantifiers of ∀x∀y(¬P(x,y)∨P(y,x))
¬P(x2,x3) ∨ P(x3,x2) would have been ¬P(a,b) ∨ P(b,a)
the leaf of the second branch is P(b,a)
once a variable is assigned, the assignment holds for the whole tableau
x2=a and x3=b in the second leaf as well
tableau can be closed by x1=x3=b
a variable is a placeholder for a term that is yet to be decided
once decided, it is the term that would have been used in a ground tableau
(except that we would have chosen f(c) without knowing it will be useful later)
rigid variable = same value in the whole tableau
violating this rule leads to unsoundness
{ ∀x(P(x)∨Q(x)), ¬P(a), ¬Q(b) }
tableau expanding the universal quantifier and the resulting disjunction
x1=a closes first branch
how about the other one?
disregard rigidity
close second branch with x1=b
(above is not a valid tableau, because...)
unsatisfiability established
but formula { ∀x(P(x)∨Q(x)), ¬P(a), ¬Q(b) } is satisfiable:
according to these values:
set is satisfiable, but disregarding the rigid variable rule the tableau method "proved" unsatisfiability
therefore: the rigid variables rule cannot be disregarded
intuitively:
the latter is like ∀x P(x) ∧ ∀y Q(y)
variables can assigned to closed terms, like x1=a
can also be assigned to unclosed terms, like x1=f(x2)
{ ∀x P(x), ∀x ¬P(f(x)) }
tableau after expanding once each universal quantifier
branch closes with x1=f(a) and x2=a
alternative: just set x1 equal to f(x2)
x1 is left partially specified
x2 is not specified at all
intuitively: whichever value x2 takes, x1 is f applied to it
advantage?
by letting x2 unspecified, other branches might be closed
example on:
{ ∀x P(x), ¬Q(f(a)), ∀x(¬P(f(x)) ∨ Q(x)) }
tableau after some obvious steps
x1=f(a) and x2=a close first branch
but...
x2 is a in the whole tableau
right leaf Q(x2) is Q(a)
Q(a) does not contradict ¬Q(f(a))
close first branch with x1=f(x2) instead
x2 left unspecified
x2 is later set to f(a) to close the second branch
use terms as unspecified as possible
principle:
make literals one the opposite of the other
using terms as unspecified as possible
given literals A and ¬B, take the most general unifier of A and B
the MGU is the most general way of making A equal to B
in fact, is the same problem: semantics of tableau
∀x ∃y P(x,y) = for each x there exists a possibly different y making P true
each x may have a different y
in the example:
x1 can be replaced by an arbitrary term
therefore:
P(x1,c) implies that P(term1,c) is true, that
P(term2,c) is true, etc.
is like saying that there exists a single, specific value for c such that P(x1,c) is true for every x1
does not work
transforms ∀x ∃y P(x,y) into ∃y ∀x P(x,y)
the problem: meaning of ∃y P(x1,y)
two facts about x1 in ∃y P(x1,y)
putting together 1 and 2:
x1 is universally quantified, but
all its occurrences in the tableau fall into the scope of the same universal quantifier
now: make intuition formal
tableau = branch ∨ branch ∨ ... ∨ branch
branch = formula ∧ formula ∧ ... ∧ formula
example:
B1 ∨ B2 ∨ B3 ∨ ( F1 ∧ F2 ∧ ∀x P(x) ∧ F4 ) ∨ B5
application of the universal quantifier rule generates a new formula in the branch:
B1 ∨ B2 ∨ B3 ∨ ( F1 ∧ F2 ∧ ∀x P(x) ∧ F4 ∧ P(x1) ) ∨ B5
the whole formula contains a free variable
when checking satisfiability, free variables are generally assumed to be existentially quantified
however, in this case we assume by a convention that derive from the intended use of tableau that they are universally quantified:
B1 ∨ B2 ∨ B3 ∨ ( F1 ∧ F2 ∧ ∀x P(x) ∧ F4 ∧ P(x1) ) ∨ B5
is intended to mean:
∀x1 ( B1 ∨ B2 ∨ B3 ∨ ( F1 ∧ F2 ∧ ∀x P(x) ∧ F4 ∧ P(x1) ) ∨ B5 )
is like renaming the variable and moving the universal quantifier to the front of the formula:
… ∀x P(x) … ⇒ … ∀x1 P(x1) … ⇒ ∀x1 … P(x1) …
formula does not contain any other occurrence of x1
⇓
semantics is unchanged
an example expansion in ground tableaux:
∀x ∃y P(x,y) ⇒ ∃ y P(f(a),y) ⇒ P(f(a),c)
(this is an example, with term f(a) for ∀x)
intuitively, P(f(a),c) is satisfiable if:
what if the universal quantifier is not removed but moved to the front of the formula?
in the new version:
… ∀x ∃y P(x,y) … ⇒ … ∀x1 ∃y P(x1,y) … ⇒ ∀x1 … ∃y P(x1,y) …
true if, for every value of x, there exists a value for y making P true
or,
there exist a function from x to y such that, for every x the corresponding value of y is such that P is true
in first-order logic, models contain the evaluation of functions
satisfiability is: there exists a model satisfying the formula;
if the formula contains a function, "there exists a model" includes
"there exists a function"
∀x1 ... ∃y P(x1,y) ... ⇒ ∀x1 ... P(x1,f(x1)) ...
∀x1 ∀x2 ... ∃ y P(x1,y) ... ⇒ ∀x1 ∀x2 ... P(x1,f(x1,x2)) ...
variable x2 does not occur in the formula P(x1,y)
irrelevant to its value (may be relevant to other formulae!)
making y depend on it is useless
∀x1 ∀x2 ... ∃y P(x1,y) ... ⇒ ∀x1 ∀x2 ... P(x1,f(x1)) ...
a branch can be closed if two of its literals can be made to match:
one literal is the converse of the second after some replacement is applied
replacement may need to be applied to both, like for: ¬Q(x1,a) and Q(b,x2)
if two literals are one the opposite of the other, close
often, variables need to be replaced with some terms in order to close
example: ¬Q(x1,a) and Q(b,x2) in the same branch mean:
∀x1 ∀x2 ... (... ∧ ¬Q(x1,a) ∧ ... ∧ Q(b,x2) ...) ...
branch can be closed by making the two literals the opposite of each other
use replacement x1=b and x2=a
formula before replacement:
∀x1 ∀x2 ... (... ∧ ¬Q(x1,a) ∧ ... ∧ Q(b,x2) ...) ...
after x1=b and x2=a:
... (... ∧ ¬Q(b,a) ∧ ... ∧ Q(b,a) ...) ...
formally, some quantifiers ∀xi ... P(...xi...) are replaced by a specific value ...P(...a...)
replacement produces a consequence of the original formula
the universal quantification rule creates P(...xi...) from ∀x P(...x...)
since xi is still universally quantified (in the front of the whole formula of the tableau), the new formula is equivalent to the original one
replacing xi with a makes ∀xi...P(...xi...) become ...P(...a...)
this weakens the formula:
the universal quantification rule produces an equivalent of the original formula; replacement weakens the new formula and all occurrences of its subformulae
when replacing variables, use the choice that constraint them the least
example: to match P(x1) and ¬P(f(x2)), do not use x1=f(a) and x2=a
use x1=f(x2) instead
weakens the formula the least possible:
may work or not
result is:
∃ y P(f(y),f(y))
this is a consequence of the original formula: instead of "for every x", this is "for the particular value f(y)"
result is:
∃y P(f(y),f(y))
in the original formula, the value of y making P true depends on x
in the resulting formula, x depends on y instead!
∀x ∃y P(x,f(y)) and ∃y P(f(y),f(y)) differ
first one = for every value v there exists another value v' such that P(v,f(v')) is true
second one = there exists a value v' such that P(f(v'),f(v')) is true
counterexample: the following model satisfies the first formula but not the second one
according to this model:
some substitution with variables work, others do not
f(y)/x did not work for ∀x ∃y P(x,f(y))
reason: makes x depend on y
(instead of the other way around)
general rule: t/x does not work if:
∀x ... | P(x) | ... | ∃y Q(x,y) |
OK | NO |
P(x1) and P(f(x1) do not unify
a replacement like f(x1)/x1) is recursive
result would be P(f(x1)) and P(f(f(x1)))
still different
is the most general substitution that makes two formulae to be the same
creates as few constraints on the variables as possible
example: P(x1) and P(f(x2)) become the same by setting:
the MGU is the second: f(x2)/x1
example on the two literals:
unification makes two literals the same
for closing a branch of a tableau, we negate one of the two
(makes literals one the opposite of the other)
proceed recursively
predicates are the same: go ahead, recursively
proceed, but remember substitution f(z)/x
f(y) and f(x) are terms built over the same function f
they match if their arguments match
proceed recursively on arguments
new substitution to be remembered: x/y
occur check violation: x is f(z) because of first substitution
cannot match with z
literals do not unify
in this example, literals do not unify
otherwise, the MGU is the union of all accumulated substitutions
in a branch, if a literal and the opposite of another unify,
apply the MGU to the whole tableau and close the branch
the MGU is free for the formula of the tableau
applying it produces a formula that is a consequence of the original one
propositional: |
|
| |||||||
first-order: |
|
| |||||||
xi is a new variable | f is a new function symbol and
x1,...,xm are the free variables in F |
closure rule:
if two literals F and ¬G on the same branch are such that F and G unify with MGU σ,then apply σ to all formulae of the tableau and close the branch
second point is not exactly what is needed
aim:
if a set is unsatisfiable, it can be proved by expanding its tableau in some way and closing all its branches
but it can be proved only that:
if a set is unsatisfiable, there exists a closed tableau for it
applying the rules in some order does not guarantee to find a closed tableau
for ground tableaux, the problem was expanding the universal quantifiers in an unfair way
for tableau with unification, the problem is: applying a substitution weakens the formula of the tableau
replacing x1 with a for closing a
branch may create problems on other branches
(example on next slide)
next: actual case
formula:
{ ¬P(a), ¬Q(c), ¬R(d), ∀x ( ( (R(d) ∨ ¬ P(b)) ∧ P(x) ) ∨ ( (R(d) ∨ ¬ Q(b)) ∧ Q(x) ) ) }
unsat:
next: expanding depth-first and applying a MGU as soon as it closes a branch
closed with x1=a
for the sake of this example, to simplify the notation:
replace x1 with a in the other branch
second branch differs from first:
Q(a) and ¬Q(c) cannot be made opposite to each other
only rule applicable at this point is expansion of universal quantifier
in the open branch, everything is as before
only difference from root is the useless literal ¬Q(b)
everything is repeated, another ¬Q(b) is generated and everything starts again
a closed tableau for the formula exists!
go back to first closure and make a different choice
tableau right before the first closure
do not close with x1=a
keep running instead
leave branch ending in ¬P(b) open
continue on the other open branch
now clear: both branches left open can be closed at same time with x1=b
conclusion: applying unification as soon as a branch can be closed by lead to incompleteness
solutions?
unification is applied only when it closes all open branches at the same time
problem: number of open branches to keep in memory,
cost of checking all of them every time
start from the initial tableau
perform in turn every expansion that can be done from it
this generates a number of other tableaux:
repeat for each of them
figure shows a propositional tableau
actually useful for first-order logic tableau with unification
{ a∧b, ¬a∨¬b }
first tableau
applying this method to first-order tableau with unification
if the formula is unsatisfiable the closed tableau will be found