On the Safe Termination of PROLOG Programs.
Krzysztof Rafal Apt, Roland N. Bol, Jan Willem Klop · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1989
We systematically study loop checking mechanisms for logic programs by considering their soundness, completeness, relative strength and related concepts.We introduce a natural concept of a simple loop check and prove that no sound and complete simple loop check exists, even for programs without function symbols.Then we introduce a number of sound simple loop checks and identify a natural class of PROLOG programs for which they are complete.In this class a limited form of recursion is allowed.As a by-product we obtain an implementation of the closed world assumption of Reiter [R] and a query evaluation algorithm for a class of logic programs without function symbols.