Information Technology Reference
In-Depth Information
A congruence closure algorithm can deduce some useful information for finite
model searching. One example is given in [8]. From the following two equations:
f(f(f(a))) = a
f(f(f(f(f(a))))) = a
we can deduce that
f(a) = a
. Thus we need not “guess” a value for
f(a)
,ifthe
above two equations are in the input clauses. Without using the congruence clo-
sure, we may have to try unnecessary assignments such as
f(a) = b, f(a) = c
,
etc., before or after the assignment of
f(a) = a
.
3.2
An Example
Let us look at a problem in the combinatorial logic. A fragment of combina-
tory logic is an equational system defined by some equational axioms. We are
interested in the fragment
{
B, N1
}
, whose axioms are:
a
(
a
(
a
(B
,x
)
,y
)
,z
)=
a
(
x, a
(
y, z
))
a
(
a
(
a
(N1
,x
)
,y
)
,z
)=
a
(
a
(
a
(
x, y
)
,y
)
,z
)
Here B and N1 are constants, while the variables
x
,
y
and
z
are universally
quantified. The
strong fixed point property
holds for a fragment of combinatory
logic if there exists a combinator
y
such that for all combinators
x
,
a
(
y, x
)=
a
(
x, a
(
y, x
))
.
In other words, the fragment has the strong fixed point property
if the formula
ϕ
:
∃y∀x
[
a
(
y, x
)=
a
(
x, a
(
y, x
))] is a logical consequence of the
equational axioms.
In [13], it is shown that the fragment
{
}
does not have the strong
fixed point property, because there is a counterexample of size 5. It is a model
of the following formulas:
B, N1
(BN1-1)
a(a(a(0,x),y),z) = a(x,a(y,z)).
(BN1-2)
a(a(a(1,x),y),z) = a(a(a(x,y),y),z).
(BN1-3)
a(y,f(y)) != a(f(y),a(y,f(y))).
The last formula is the negation of the formula
ϕ
,where
f
is a Skolem function
and
!=
means “not equal”. In the first two formulas, we assume that B is 0
and N1 is 1. That is, B and N1 take different values. (But it is also possible to
generate a counterexample in which B = N1.)
Search by SEM.
When using the standard version of SEM [16], the first few
steps of the search tree are the following:
(1) Choose the cell
a(0,0)
and assign the value 0 to it.
(2) Choose the cell
f(0)
and assign the value 1 to it. Note that
f(0)
cannot
be
0
; otherwise the formula (BN1-3) does not hold, because we already have
a(0,0) = 0
.
Search WWH ::
Custom Search