%% author=      Marija Kulas
%% date=        18 May 2005
%% homepage=    http://www.fernuni-hagen.de/pi8/mk


@InProceedings{KulasM:towcb,
  author =      {M.~Kula\v{s}},
  title =       {Toward the concept of backtracking computation},
  booktitle =   {Proc. of the Workshop on Structural Operational Semantics (SOS'04), London},
  editor =      {L.~Aceto and W.~J.~Fokkink and I.~Ulidowski},
  series =      {ENTCS}, 
  volume =      {128, issue 1},
  pages =       {39-59}, 
  publisher =   {Elsevier},
  year =        {2005},
  doi =         {doi:10.1016/j.entcs.2004.10.026}, 
url={ http://www.cs.auc.dk/~luca/SOS-WORKSHOP },
abstract={ This article proposes a new mathematical definition of the 
execution of pure Prolog, in the form of axioms in a structural operational
semantics. The main advantage of the model is its ease in representing
backtracking, due to the functionality of the transition relation and
its converse. Thus, forward and backward derivation steps are possible.
A novel concept of stages is introduced, as a refinement of final
states, which captures the evolution of a backtracking computation. 
An advantage over the traditional stack-of-stacks approaches is a
modularity property. Finally, the model combines the intuition of the
traditional `Byrd box' metaphor with a compact representation of
execution state, making it feasible to formulate and prove theorems
about the model. In this paper we introduce the model and state some
useful properties. } }


@InProceedings{KulasM:purpe,
  author =      {M.~Kula\v{s}},
  title =       {Pure {P}rolog Execution in 21 Rules},
  booktitle =   {Proc. of the 5th Workshop on Rule-Based Constraint Reasoning and Programming (RCoRP'03), Kinsale},
  year =        {2003},
  month =       {September},
url={ http://www.univ-orleans.fr/SCIENCES/LIFO/Members/lallouet/rcorp03 },
abstract={ A simple mathematical definition of the 4-port model for pure 
Prolog is given. The model combines the intuition of ports with a compact
representation of execution state. Forward and backward derivation
steps are possible. The model satisfies a modularity claim, making it
suitable for formal reasoning. } }


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


@InProceedings{KulasM:rewps,
  author =      {M.~Kula\v{s}},
  title =       {A Rewriting {P}rolog Semantics},
  booktitleXX = {Proc. of the CL 2000 Workshop on Verification and Computational Logic (VCL 2000), London},
  booktitle =   {Proc. of VCL 2000, London},
  editor =      {M.~Leuschel and A.~Podelski and C.~R.~Ramakrishnan and U.~Ultes-Nitsche},
  year =        {2000},
  note =        {Southampton University Tech. Report DSSE-TR-2000-6}, 
url={ http://www.ecs.soton.ac.uk/~mal/vcl2000.html },
abstract={ We introduce a lean and intuitive operational semantics of a
characteristic subset of Standard Prolog (the whole logic and control,
database updates and solution collecting). The Prolog computation is
modelled as conditional rewriting of derivation states. Due to a novel
linear representation of the Prolog tree traversal, our approach is
especially suitable for modelling the control flow. The semantics is
fully operational and implemented in Prolog. } }


@InProceedings{KulasM:annpcr,
  author =      {M.~Kula\v{s}},
  title =       {Annotations for {P}rolog -- {A} Concept and Runtime Handling},
  booktitle =   {Logic-Based Program Synthesis and Transformation. Selected Papers of the 9th Int. Workshop (LOPSTR'99), Venezia},
  editor =      {A.~Bossi},
  volume =      {1817},
  series =      {LNCS},
  year =        {2000},
  publisher =   {Springer-Verlag},
  pages =       {234--254},
url={ http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-67628-7 },
abstract={ A concept of annotations for rendering procedural aspects of
Prolog is introduced, built around well-known procedural concepts of
Standard Prolog. Annotations describe properties of predicates. Such
properties can be pre or post conditions, which must hold true when a
predicate is called or exited, respectively. We introduce two more kinds of
annotations, fail and redo annotations, hence incorporating a whole
model of Prolog execution into our language. This enables natural
rendering of many procedural properties of Prolog which cannot be expressed
with only pre/post conditions, like non-failure. Every annotation can be
narrowed down to a subset of calls, via calling premiss. With the
novel idea of context we supersede program-point assertions. The
annotations are defined simply as Prolog goals, making them fully
parametric and therefore comfortable for debugging. All examples
presented are actual runs of our system Nope. } }


@InProceedings{KulasM:debpua,
  author =      {M.~Kula\v{s}},
  title =       {Debugging {P}rolog Using Annotations},
  booktitleXX = {Proc. of the 10th Workshop on Logic Programming Environments (WLPE'99), Las Cruces, NM},
  booktitle =   {Proc. of WLPE 1999}, 
  editor =      {M.~Ducass\'{e} and A.~Kusalik and G.~Puebla},
  volume =      {30, issue 4},
  series =      {Electronic Notes in Theoretical Computer Science},
  publisher =   {Elsevier},
  year =        {2000},
url={ http://www.elsevier.com/locate/entcs },
abstract={ We present an annotation language well suited for rendering
aspects of Prolog execution. Our annotations are special Prolog goals
that act as executable comments, performing debugging at run-time. No
restrictions are placed upon the object language, the concern being
verification of (full) Standard Prolog programs. Here we discuss the
merits of the annotations for Prolog debugging. All the examples are
actual runs of our system Nope. } }