Information Technology Reference
In-Depth Information
The paper is organized as follows. Section 2 defines the pattern unification
algorithm, and in section 3 its correctness and completeness is proved. Section 4
presents the proof search algorithm, and again its correctness and completeness
is proved. The final section 5 contains what we have to say about extensions to
∧
and
∃
.
2
The Unification Algorithm
We work in the simply typed
-calculus, with the usual conventions. For instance,
whenever we write a term we assume that it is correctly typed.
Substitutions
are denoted by
λ
ϕ, ψ, ρ
. The result of applying a substitution
ϕ
to a term
t
or a formula
, with the understanding that after the
substitution all terms are brought into long normal form.
Q
A
is written as
tϕ
or
Aϕ
always denotes a
∀∃∀
-prefix, say
∀
x
∃
y
∀
z
, with distinct variables. We call
x
the
signature variables
,
y
the
flexible variables
and
z
the
forbidden variables
of
Q
,andwrite
Q
∃
for the existential part
∃
y
of
Q
.
Q
-terms
are inductively defined by the following clauses.
-
If
u
is a universally quantified variable in
Q
or a constant, and
r
are
Q
-terms,
then
u
r
is a
Q
-term.
-
For any flexible variable
y
and distinct forbidden variables
z
from
Q
,
y
z
is
a
Q
-term.
-
If
r
is a
Q∀z
-term, then
λzr
is a
Q
-term.
Explicitely,
r
is a
Q
-term iff all its free variables are in
Q
, and for every subterm
y
r
of
r
with
y
free in
r
and flexible in
Q
,the
r
are distinct variables either
λ
-bound in
r
(such that
y
r
is in the scope of this
λ
) or else forbidden in
Q
.
Q
-goals
and
Q
-clauses
are simultaneously defined by
-
If
r
are
Q
-terms, then
P
r
is a
Q
-goal as well as a
Q
-clause.
-
If
D
is a
Q
-clause and
G
is a
Q
-goal, then
D → G
is a
Q
-goal.
G
Q
D
Q
G → D
Q
-
If
is a
-goal and
is a
-clause, then
is a
-clause.
-
If
G
is a
Q∀x
-goal, then
∀xG
is a
Q
-goal.
-
If
D
[
y
:=
Y
z
]isa
∀
x
∃
y
,Y∀
z
-clause, then
∀yD
is a
∀
x
∃
y
∀
z
-clause.
A
Q
Q
Explicitely, a formula
is a
-goal
iff all its free variables are in
,andfor
y
r
A
y
A
y
r
every subterm
of
with
either existentially bound in
(with
in the
scope) or else free in
A
and flexible in
Q
,the
r
are distinct variables either
λ
-
or universally bound in
A
(such that
y
r
is in the scope) or else free in
A
and
forbidden in
Q
.
A
Q
-substitution
is a substitution of
Q
-terms.
A
unification problem
U
consists of a
∀∃∀
-prefix
Q
and a conjunction
C
of
-terms of the same type, i.e.,
i
=1
r
i
=
equations between
Q
s
i
. We may assume
that each such equation is of the form
λ
x
r
=
λ
x
s
with the same
x
(which may
be empty) and
of ground type.
A
solution
to such a unification problem
r, s
U
is a
Q
-substitution
ϕ
such that
for every
i
,
r
i
ϕ
=
s
i
ϕ
holds (i.e.,
r
i
ϕ
and
s
i
ϕ
have the same normal form). We
Search WWH ::
Custom Search