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 pf 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