**Author: Kouichi Hirata**.

**Source: ***Lecture Notes in Artificial Intelligence* Vol. 1720,
1999, 157 - 168.

**Abstract.**
*Flattening* is a method
to make a definite clause function-free.
For a definite clause *C*,
flattening replaces every occurrence of a term
in *C*
with a new variable *v* and
adds an atom
with the associated predicate symbol p_{f} with *f*
to the body of *C*.
Here, we denote the resulting function-free definite clause from *C*
by .
In this paper,
we discuss the relationship between flattening
and implication.
For a definite program and a definite clause *D*,
it is known that
if
then ,
where is the set of
for each .
First,
we show that the converse of this statement does not hold
even if , that is, there exist definite clauses
*C* and *D* such that
but .
Furthermore,
we investigate the conditions of *C* and *D* satisfying
that if and only if .
Then,
we show that, if (1) *C* is not self-resolving
and *D* is not tautological,
(2) *D* is not ambivalent,
or (3) *C* is singly recursive,
then the statement holds.

©Copyright 1999 Springer-Verlag