Negation as failure. Completeness of the query evaluation process for Horn clause programs with recursive definitions (Q1101250)

An extension of the class of logic programs for which the negation as failure rule is equivalent to the closed world assumption is presented. This extension includes programs on infinite domains and with recursive definitions. For this class of programs with ground (positive or negative) queries the query evaluation process is complete. A characterization of this class of programs is given, and a decision algorithm, which recognizes a subclass of these programs, is presented. The algorithm is based on showing the correspondence between a program and a primitive recursive function.