Defining Standard Prolog in Rewriting Logic
Marija Kulaš, Christoph Beierle · Electronic Notes in Theoretical Computer Science · 2000
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.