A high-level Petri net for goal-directed semantics of Horn Clause Logic

A new high-level Petri net (HLPN) model is introduced as a graphical syntax for Horn Clause Logic (HCL) programs. We call these nets: Horn Clause Logic Coal-Directed Nets (HCLGNs). It is shown that there is a bijection between the queried definite programs and the class of HCLGNs. In addition, a visualization of SLD-resolution is realized through the enabling and firing rules and net markings. The correctness of these rules with respect to SLD-resolution is also proven. Using these notions, we model SLD-refutations and failing computations. Through minor modification of the definition of HCLGNs for pure HCL programs and of the enabling and firing rules, it is shown how HCLGNs can be used to model built-in atoms and provide a new AND/OR-parallel execution model. HCLGNs have also been used to: model a subset of Prolog; provide a framework for modeling variations on SLD-resolution, such as SLD-ALG; specify an operational semantics for committed-choice (flat-guarded) concurrent logic languages using FGHC as an example. Recently, several software packages have become available for editing and executing HLPNs. These graphical editors can now play the same role that string editors have played for many years. The simulation capabilities of the HLPN software offer opportunities to perform automated, interactive code walk-throughs and also have potential for providing a framework for visual debugging environments. We note however that HCLGNs differ from the major classes of HLPNs for which software tools have been developed in primarily two ways: 1) the tokens in the markings can have variables; and 2) the firing of a transition may not only update the marking of the adjacent places, but may instantiate variables in tokens in the markings of places that are non-adjacent to the fired transition. Thus, the existing packages can only provide graphical syntax editing and are not appropriate for graphical simulation of HCLGNs. In the paper, we provide an algebraic characterization of HCLGNs that can serve as a design guideline for implementing HCLGNs.