On the existence of nonterminating queries for a restricted class of PROLOG-clauses

摘要

This work studies the existence of nonterminating queries for a restricted class of recursive predicates. The class is restricted to predicates defined by a set of clauses containing only one (direct) recursive clause. Moreover, this clause must be of the form P(…):-P(…). For this restricted class of predicates, we prove a necessary and sufficient condition for the existence of a query which is nonterminating in the absence of the occur check. The condition is based upon concepts from rational trees.