@InProceedings{KulasBeierle:defsp,
  author = 	 {M.~Kula\v{s} and C.~Beierle},
  title = 	 {Defining {S}tandard {P}rolog in Rewriting Logic},
  booktitle = 	 {Proc. of the 3rd Int. Workshop on Rewriting Logic and
its Applications (WRLA'2000), Kanazawa},
  editor =   	 {K.~Futatsugi},
  series = 	 {Electronic Notes in Theoretical Computer Science},
  volume = 	 {36},
  publisher =    {Elsevier},
  year = 	 {2001},
  note = 	 {http://www.elsevier.nl/locate/entcs/volume36.html},
  url={http://www.elsevier.nl/locate/entcs/volume36.html},
abstract={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. }  }