Mathematical characterization of finite failure
Christopher John Hogger · 1990
Abstract Theme 46 established that, for any definite program P, there exists a particularly simple way of constructing its success set SS(P) using the Tp function: starting with the bottom element ¢ in our lattice of interpretations, repeated application of this function generates a monotonically-increasing chain It so happens that there is a somewhat similar method of constructing the finite failure set FF(P). In order to appreciate its rationale it is useful to understand clearly the process by which a ground query ?q finitely fails from a definite program P. In particular we need to consider the depth within which the failure occurs. The simplest way for ?q to fail finitely is for there to be no clause in P whose heading unifies with q-equivalently, for there to be no clause in G(P) having q as its heading. In this case the failure is said to occur within depth k=l. Relative to the given program P there may be many atoms qEB(P) for which this is so. The set of all such atoms is denoted by FF(P, 1) and can be characterized very easily using the