Flattening and Implication

Abstract

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 pf ( t _1, . . . , t _n, v ) 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 flat(C) . 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 flat(П) ⊨ flat(D) then П ⊨ D , where flat(П) is the set of flat(C) for each C ∈ П . First, we show that the converse of this statement does not hold even if П = 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.