Flattening and Implication

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 $f(t_1,\cdots,t_n)$ in C with a new variable v and adds an atom $p_f(t_1,\cdots,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 ${\it flat\/}(C)$ . In this paper, we discuss the relationship between flattening and implication. For a definite program $\Pi$ and a definite clause D, it is known that if ${\it flat\/}(\Pi)\models{\it flat\/}(D)$ then $\Pi\models D$ , where ${\it flat\/}(\Pi)$ is the set of ${\it flat\/}(C)$ for each $C\in\Pi$ . First, we show that the converse of this statement does not hold even if $\Pi = \{C\}$ , that is, there exist definite clauses C and D such that $C\models D$ but ${\it flat\/}(C)\not\models{\it flat\/}(D)$ . Furthermore, we investigate the conditions of C and D satisfying that $C\models D$ if and only if ${\it flat\/}(C)\models{\it 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.