text: We address the problem of complementing higher-order patterns without repetitions of existential variables. Differently from the first-order case, the complement of a pattern cannot, in general, be described by a pattern, or even by a finite set of patterns. We therefore generalize the simply-typed λ-calculus to include an internal notion of strict function so that we can directly express that a term must depend on a given variable. We show that, in this more expressive calculus, finite sets of patterns without repeated variables are closed under complement and intersection. Our principal application is the transformational approach to negation in higher-order logic programs.
  @cite_22: Abstract A transformation technique is introduced which, given the Horn-clause definition of a set of predicates p i , synthesizes the definitions of new predicate p i which can be used, under a suitable refutation procedure, to compute the finite failure set of p i . This technique exhibits some computational advantages, such as the possibility of computing nonground negative goals still preserving the capability of producing answers. The refutation procedure, named SLDN refutation, is proved sound and complete with respect to the completed program.
summary: Lassez87 proposed the seminal algorithm for computing relative complements and introduced the now familiar restriction to linear terms. We quote the definition of the @math '' algorithm for the (singleton) complement problem given in @cite_22 which we generalize in Definition . Given a finite signature @math and a linear term @math they define: [ ] The relative complement problem is then solved by composing the above complement operation with term intersection implemented via first-order unification.