M. Kulas and C. Beierle. Defining Standard Prolog in rewriting logic. In K. Futatsugi, editor, Proc. of the 3rd Int. Workshop on Rewriting Logic and its Applications (WRLA'2000), Kanazawa, volume 36 of Electronic Notes in Theoretical Computer Science. Elsevier, 2001. http://www.elsevier.nl/locate/entcs/volume36.html.
The coincidence between the model-theoretic and the procedural semantics of SLD-resolution does not carry over to a Prolog system that also implements non-logical features like cut and whose depth-first search strategy is incomplete. The purpose of this paper is to present the key concepts of a new, simple operational semantics of Standard Prolog in the form of rewriting rules. We use a novel linear representation of the Prolog tree traversal. A derivation is represented at the level of unification and backtracking. The rewriting system presented here can easily be implemented in a rewriting logic language, giving an executable specification of Prolog.