Appeared in Volume 7/1, February 1994
16th November 1993
A little while ago, I asked for some references on the implementation of fair search rules and WAM-like abstract machines for complete Horn solvers. I also wondered how these things could be related to goal freezing. Here is a summary of the replies and references that I received. Thanks to everybody that replied.
Frederic Mesnard (firstname.lastname@example.org): In , I show how it is possible to automatically generate freeze declaration from the text of the programs to ensure (depth-first) termination of CLP programs.
Since it also has an optional occur check mode, ECLiPSe in fact gives you a
complete Horn solver. ECLiPSe documentations can be obtained from:
2. Richard E. Korf, Iterative-Deepening-A*: An Optimal Admissible Tree Search, Proc. of the Ninth IJCAI, pp.1034-1036, Los Angeles, California, August, 1985
3. Richard E. Korf, Depth-First Iterative-Deepening: An Optimal Admissible Tree Search, Artificial Intelligence, pp.97-109, 1985, Vol.27
4. Mark E. Stickel and W. Mabry Tyson, An Analysis of Consecutively Bounded Depth-First Search with Applications in Automated Deduction, Proc. of the Ninth IJCAI pp.1073-1075, Los Angeles, California, August, 1985
5. Lee Naish, Negation and control in Prolog, LNCS 238, Springer-Verlag, New York, 1986
6. Termination of Constraint Logic Programs, by Means of Approximations, Fred Mesnard, Ph.D. thesis, Universite Paris VI, 1993, January, Written in french.
We first present a class of mappings, called approximations, between constraint LP languages, which allow us to focus on the images Pb in CLP(Bool), and Pq in CLP(Q), of an initial program P.
We study Pb in order to get some knowledge about the state of the variables of a goal once it has been proved.
From Pq, and with the help of a technique due to Sohn and Van Gelder, we bring to light linear terms decreasing at each recursive call.
Then we show how :
Michael Jampel (email@example.com)
Alan Smaill (firstname.lastname@example.org)
Jens E Wunderwald (email@example.com)
20th December 1993
I haven't received any more comments since I posted the summary. I successfully used the ECLiPSe system (which is very good), but I didn't find any references in the documentation to the additional WAM instructions that manipulate the depth. However, the als/1 predicate of ECLiPSe prints out an almost readable WAM listing of the generated code, and thus gives some hints about the DFID compilation.