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: Speaking in terms of resolution, the resolvent of ¬a and (a ∨ ¬a) is again ¬a, and so it continues if we simply blindly try to derive ⊥ and do not check for saturation of derived clauses. This program is also not subject to occurs check (s.t.o), so occurs check does not solve the problem either even though it is in itself a good idea to use.
Memoization in the sense of "remembering what has already been derived" does not improve termination either in this case, since nothing has been derived yet. You can easily implement a simple form of memoization within Prolog, but SLG resolution goes well beyond that and can improve not only performance but in fact even termination characteristics, as the above example shows.
An interesting reference that may serve as a useful starting point to implement tabling is the paper Tabling as a Library with Delimited Control by Desouter et al.:
https://biblio.ugent.be/publication/6880648/file/6885145.pdf
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!
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!
Does SLDNF really not terminate in cases that produce a cyclic answer or is it the subsequent step that replaces instantiated variables with values that will not terminate? E.g. the step that prints frames? In the latter case, would an occurs check solve the problem?
How is tabling different from SLD with memoization? If this is too complicated to explain in passing, pointers to literature would be welcome!