This is a very important feature of Strawberry Prolog which we expect to be available one day.

The idea of Loop Checking is coming from the difference between declarational and procedural semantic of Prolog programs. When you write a program you think in declarational semantic. You think of the program like a set of axioms and rules and you want to obtain all answers which follow from them. Unfortunately, the Prolog Interpreter works in the procedural semantic and gives you only a part of the answers, after that it can fail in infinite loop. Our purpose is to give you the opportunity to write some declaratively correct, but procedurally incorrect programs. The loop checker will make them running correct in the declarative sense which you have put in them.

It is nice how the class of the programs which are working correctly (in the declarational sense) is maximally big. That is why we are searching for an effective algorithm which recognizes a big amount of cyclings in Prolog. The purpose is to add this algorithm to our Prolog interpreter. In this way we will obtain an interpreter of the language stronger than Prolog, because cycling in Prolog programs will work and give the expected answer.

The Loop Checker will be realized on the basis of the works of Professor Dimiter Skordev and those of the author which he made under the supervision of Professor Skordev. Users of Strawberry Prolog who are interested in this problem can read the implementor's master's thesis "Periodical Cyclings in Prolog", that is available on our web page.