> SLDNF resolution really does not terminate in many cases, also if no variables at all are involved. The "a :- a." example which I mentioned is such a case [...]

I see! In a hurry, my mind substituted "A :- A.", but your example is indeed more interesting than that! Now I am curious as to how SLG resoultion deals with this case. This is definitely something I will look into at some point! At the moment I am at a stage where I am happy that my retract/1 implementation is respecting the logical view. :)

> I'm looking forward to seeing more papers and slides from you about these topics, and to discussing them here, keep up the nice work!

Thank you!