Loop detection in propositional Prolog programs

Abstract

We are interested in loop detection in knowledge based systems because loops are one of the problems when formalizing knowledge. Since rule-based systems are widely used and backward chaining in rule-based systems and the Prolog inference-strategy for logic programs can be compared, we consider loop detection in propositional Prolog-programs.

First we present an algorithm which decides for a given Prolog-program π and a query γ, whether the answer is yes, no or loop. We prove that this algorithm needs linear time in the length of π∧γ. This is possible by setting a flag for each atom occuring in π, which reflects the actual state of this atom during the refutation. We show that the algortihm can be extended to Prolog-programs π^c with cut.

Further we show that the problem to decide, whether there exists a query for a given Prolog-program (including cut) which leads to a looping derivation, is NP-complete.

Allowing assert and retract in a propositional Prolog-program we show that the loop-problem is undecidable. In this case it is even undecidable whether we obtain a looping refutation for a given question γ and a Prolog-program π^ar.

The work of this author was supported by the Studienstiftung des deutschen Volkes