Plattening and Implication

摘要

Flattening is a method to make a definite clause function-free. For a definite clause C, flattening replaces every occurrence of a term f(t_1,...,t_n) in C with a new variable v and adds an atom p_f( t_1,...,t_n,v) 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 flat (C). In this paper, we discuss the relationship between flattening and implication. For a definite program II and a definite clause D, it is known that if flat(II) |= flat (D) then II |= D, where flat(II) is the set of flat(C) for each C implied by II. First, we show that the converse of this statement does not hold even if II = {C}, that is, there exist definite clauses C and D such that C |= D but flat (C) flat (D). Furthermore, we investigate the conditions of C and D satisfying that C |= D if and only if flat (C) |= flat (D). 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.