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(t1,…, tn) in C with a new variable v and adds an atom pf (t1,…, tn, 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 Cand 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) Dis not ambivalent, or (3) C is singly recursive, then the statement holds.