Tableaux with unification

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?


Choice of term

the idea is:

do not choose t

apply the rule ∀x F/F[t/x] but leave t unspecified


Delayed choice: example

{∀x P(x), ¬P(f(a))}

preliminary version shown for illustration

actual method: later


First step

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)


Unspecified term

P(  ) is not a valid formula

label for: P(something)
where "something" is to be decided

now?


Choice of term

branch can be closed by choosing f(a) as the term that was unspecified


Closure

put f(a) in P(  )

branch (and tableau, in this case) can be closed


Another example

{∀x P(x), ∃x (¬P(x) ∨ ¬P(f(x)))}


First step

general rule is to expand existential quantifiers first

for the sake of this example, we do the converse


Example, first unspecified formula

the argument to P is left void

will be chosen later


Two steps more

after expanding the existential quantifier and the disjunction

P( ) is still empty (term to be decided)

what to put in is now clear


Choice of term

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


Closure

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


Second expansion of universal quantifier

tableau after expanding the universal quantifier a second time


Closure

if P( ) is filled with f(c), the second branch can be closed


Wrong choice at the beginning

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


Unspecified terms: principles and problems

principles:

problems:


Variables as placeholders

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


Variables: example

expand ∀P(x)

instead of P(   ) use a new variable x1 as a placeholder


New variable

P(x1) means: P applied to a term that will be chosen later


Variables: example (2)

expanded as usual


Variables: example (3)

x1=c closes first branch


Variables: example (4)

second branch would be closed by x1=f(c)...

... but cannot, because x1 has already been decided to be c


Variables: example (5)

no point in using x1 again to expand ∀x P(x)
(already assigned to c)

new placeholder for a new term; new variable


Variables: example (6)

second branch can be closed by choosing f(c) for x2


Tableau with variables: principles


Rigid variables: example

next example illustrates a concept about the values chosen for variables
(not just an example)


Rigid variables: example (1)

{ ∀x ¬P(x,a), P(a,b), ∀x∀y (P(x,y) → P(y,x)) }


Rigid variables: example (2)

tableau after some steps

first branch (leaf ¬P(x2,x3)) closes with:
x2=a and x3=b


Rigid variables: example (3)

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)


Rigid variables: example (4)

once a variable is assigned, the assignment holds for the whole tableau

x2=a and x3=b in the second leaf as well


Rigid variables: example (5)

tableau can be closed by x1=x3=b


Rigid variables

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 variables

rigid variable = same value in the whole tableau

violating this rule leads to unsoundness


Rigid variables: counterexample

{ ∀x(P(x)∨Q(x)), ¬P(a), ¬Q(b) }


Rigid variables: counterexample (1)

tableau expanding the universal quantifier and the resulting disjunction


Rigid variables: counterexample (2)

x1=a closes first branch

how about the other one?


Rigid variables: counterexample (3)

disregard rigidity

close second branch with x1=b

(above is not a valid tableau, because...)


Rigid variables: counterexample (4)

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


Rigid variables: counterexample (5)

intuitively:

the latter is like ∀x P(x) ∧ ∀y Q(y)


Unclosed terms

variables can assigned to closed terms, like x1=a

can also be assigned to unclosed terms, like x1=f(x2)


Unclosed terms: example

{ ∀x P(x), ∀x ¬P(f(x)) }


Unclosed terms: example (1)


Unclosed terms: example (2)

tableau after expanding once each universal quantifier

branch closes with x1=f(a) and x2=a

alternative: just set x1 equal to f(x2)


Unclosed terms: example (3)

x1 is left partially specified

x2 is not specified at all

intuitively: whichever value x2 takes, x1 is f applied to it

advantage?


Unclosed terms: advantage

by letting x2 unspecified, other branches might be closed

example on:

{ ∀x P(x), ¬Q(f(a)), ∀x(¬P(f(x)) ∨ Q(x)) }


Unclosed terms: advantage

tableau after some obvious steps

x1=f(a) and x2=a close first branch

but...


Unclosed terms: advantage

x2 is a in the whole tableau

right leaf Q(x2) is Q(a)

Q(a) does not contradict ¬Q(f(a))


Unclosed terms: advantage

close first branch with x1=f(x2) instead
x2 left unspecified

x2 is later set to f(a) to close the second branch


Unclosed term: general rule

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


Tableau with unification: left to do

in fact, is the same problem: semantics of tableau


Skolemization

∀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


Skolemization by constants

does not work

transforms ∀x ∃y P(x,y) into ∃y ∀x P(x,y)

the problem: meaning of ∃y P(x1,y)


Meaning of free variables

two facts about x1 in ∃y P(x1,y)

  1. possible values of x1:
  2. rigidity of variables has to be taken into account:

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


Formula of a tableau

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) ∧ F4P(x1) ) ∨ B5

the whole formula contains a free variable


Free variables in the formula

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) ∧ F4P(x1) ) ∨ B5

is intended to mean:

∀x1 ( B1 ∨ B2 ∨ B3 ∨ ( F1 ∧ F2∀x P(x) ∧ F4P(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


Skolemization on universally quantified formulae

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?


Skolemization on universally quantified formulae

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)) ...


Skolemization: simplification

∀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)) ...


Closure

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)


Closure, formally

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


Closure, semantically

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


Weakening

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


Weakening: effects

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:


Substitutions with variables

may work or not

works:
∃y ∀x P(x,f(y))
replace x with f(y)

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)"

does not work:
∀x ∃y P(x,f(y))
replace x with 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!


Substitution with variables: why not

∀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:


Free substitutions

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:


Free substitutions: example


Occurs check

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


Most general unifier

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


Unification algorithm

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


Unification algorithm (1)

predicates are the same: go ahead, recursively


Unification algorithm (2)

proceed, but remember substitution f(z)/x


Unification algorithm (3)

f(y) and f(x) are terms built over the same function f

they match if their arguments match

proceed recursively on arguments


Unification algorithm (4)

new substitution to be remembered: x/y


Unification algorithm (5)

occur check violation: x is f(z) because of first substitution

cannot match with z

literals do not unify


Unification algorithm: result

in this example, literals do not unify

otherwise, the MGU is the union of all accumulated substitutions


Unification: use for tableaux

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


Tableaux with unification: rules

propositional:
A ∧ B
A
B
A ∨ B
A | B
first-order:
∀x F
F[xi/x]
∃x F
F[f(x1,...,xm)/x]
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

Soundness and completeness

second point is not exactly what is needed


Completeness

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


Completeness: the problem

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)


Example of incompleteness

next: actual case


Incompleteness: example

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


Incompleteness: example (1)


Incompleteness: example (2)


Incompleteness: example (3)


Incompleteness: example (4)


Incompleteness: example (5)

closed with x1=a

for the sake of this example, to simplify the notation:

replace x1 with a in the other branch

Incompleteness: example (6)


Incompleteness: example (7)

second branch differs from first:
Q(a) and ¬Q(c) cannot be made opposite to each other


Incompleteness: example (8)


Incompleteness: example (9)

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


Incompleteness: example (10)

a closed tableau for the formula exists!

go back to first closure and make a different choice


Incompleteness: example (11)

tableau right before the first closure

do not close with x1=a

keep running instead


Incompleteness: example (12)


Incompleteness: example (13)

leave branch ending in ¬P(b) open

continue on the other open branch


Incompleteness: example (14)


Incompleteness: example (15)


Incompleteness: example (16)

now clear: both branches left open can be closed at same time with x1=b


Greedy unification

conclusion: applying unification as soon as a branch can be closed by lead to incompleteness

solutions?


Final closure

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


Search in the space of tableaux

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


Search in the space of tableau: example

figure shows a propositional tableau

actually useful for first-order logic tableau with unification

{ a∧b, ¬a∨¬b }


Search in the space of tableau: example (1)

first tableau


Search in the space of tableau: example (2)


Search in the space of tableau: example (3)


Search in the space of tableau: example (4)


Search in the space of tableau: example (5)

applying this method to first-order tableau with unification
if the formula is unsatisfiable the closed tableau will be found


Search in the space of tableau: implementation