This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A High-Level Petri Net for Goal-Directed Semantics of Horn Clause Logic
April 1996 (vol. 8 no. 2)
pp. 241-259

Abstract—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 Goal-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.

[1] J. Barklund, N. Hagner, and M. Wafin, "Condition Graphs," Proc. Fifth Int'l Conf. Logic Programming, pp. 435-446. MIT Press, 1988.
[2] Implementations of Prolog, J.A. Campbell, ed. Great Britain: Ellis-Horwood, 1984.
[3] T.Y. Chen, J-L. Lassez, and G.S. Port, "Maximal Unifiable Subsets and Minimal Non-Unifiable Subsets," New Generation Computing, vol. 4, pp. 133-152, 1986.
[4] J.S. Conery, Parallel Execution of Logic Programs.Boston: Kluwer Academic, 1987.
[5] S.K. Debray, "Static Inferences of Modes and Data Dependencies in Logic Programs," ACM Trans. Programming Languages and Systems, vol. 11, no. 3, pp. 418-450, 1989.
[6] C.J. Ferguson, "An Implementation of Prolog in C," Master's thesis, Dept. of Computer Science, Univ. of Waterloo, 1977.
[7] T. Fukuzawa and H. Hasegawa, "An Analysis of Parallel Programs by Utilizing High-Level Nets," 1991 Proc. IEEE Int'l Symp. Circuits and Systems, vol. 2(of 5), pp. 842-845, 1991.
[8] J.H. Gallier, Logic for Computer Science.New York: Harper&Row, 1986.
[9] J.H. Gallier and S. Raatz, "Logic Programming and Graph Rewriting," 1985 Proc.IEEE Symp. Logic Programming, pp. 208-219,Boston, 1985.
[10] H.J. Genrich, "Predicate/Transition Nets," Advances in Petri Nets 1986, Part I, Lecture Notes in Computer Science, Vol. 254, W. Bauer, W. Reisig, and G. Rozenberg, eds., Springer-Verlag, Heidelberg, Germany, 1987, pp. 208-247.
[11] J. Jeffrey, "High-Level Petri Net Semantics of Concurrent and Non-Concurrent Logic Programs," PhD dissertation, Dept. of Electrical Eng. and Computer Science, Univ. of Illinois at Chicago, 1993.
[12] J. Jeffrey and T. Murata, "A High-Level Petri Net Model for a Subset of FGHC," Proc. Second Int'l Conf. Software Eng. and Knowledge Eng., pp. 260-266. World Scientific Press, 1990.
[13] J. Jeffrey and T. Murata, "Toward Using High-Level Petri Nets to Model Declarative and Operational Semantics of Concurrent and Parallel Logic Languages," Proc. Workshop on Concurrent Logic Programs (ICLP91), June 1991.
[14] K. Jensen, "Coloured Petri Nets," Lecture Notes in Computer Science, vol. 254, pp. 248-299.New York: Springer-Verlag, 1987.
[15] High-level Petri Nets: Theory and Applications K. Jensen and G. Rozenberg, eds. New York: Springer-Verlag, 1991.
[16] R. Kowalski, "A Proof Procedure Using Connection Graphs," J. ACM vol. 22, no. 4, pp. 572-595, Dec. 1975.
[17] R. Kowalski, "Algorithm = Logic + Control," Comm. ACM, vol. 22, July 1979.
[18] J.W. Lloyd, Foundations of Logic Programming, Springer Series in Symbolic Computation, second ed. New York: Springer-Verlag, 1987.
[19] Design/CPN An noucement, Feb. 1990, Meta Software Corporation, 150 Cambridge Park Dr., Cambridge, MA 02140.
[20] T. Murata, “Petri Nets: Properties, Analysis and Application,” Proc. IEEE, vol. 77, no. 4, 1989.
[21] T. Murata, V.S. Subrahmanian, and T. Wakayama, "A Petri Net Model for Reasoning in the Presence of Inconsistency," IEEE Trans. Knowledge and Data Eng., Vol. 3, No. 3, Sept. 1991, pp. 281-292.
[22] T. Murata and D. Zhang, "A Predicate-Transition Net Model for Parallel Interpretation of Logic Programs," IEEE Trans. Software Eng., Vol. 14, No. 4, Apr. 1988, pp. 481-497.
[23] S. Raatz, Graph-Based Proof Procedures for Horn Clauses.Boston: Birkhauser, 1990.
[24] R. Ramesh, I.V. Ramakrishnan, and D.S. Warren, "Automata-Driven Indexing of Prolog Clauses," Proc. 17th Ann. ACM Symp. Principles of Programming Languages, pp. 281-291, 1990.
[25] E. Shapiro, "The Family of Concurrent Logic Programming Languages," Computing Surveys, vol. 21, no. 3, pp. 413-510, Sept. 1989.
[26] H. Tamaki and T. Sato, "OLD Resolution with Tabulation," Proc. Third Int'l Conf. Logic Programming (Lecture Notes in Computer Science), vol. 225, pp. 84-98. Springer-Verlag, 1986.
[27] K. Ueda, "Guarded Horn Clauses: A Parallel Logic Programming Language with the Concept of a Guard," ICOT Tech. Rep. TR-208, Inst. for New Generation Computer Tech nology, Tokyo, 1986.
[28] M. van Emden, "An Interpreting Algorithm for Prolog Programs," Proc. First Int'l Conf. Logic Programming Conf., 1982.
[29] L. Veille, "Database-Complete Proof Procedures Based on SLD Resolution," Proc. Fourth Int'l Conf. Logic Programming, pp. 74-103. MIT Press, 1987.
[30] D. Zhang and T. Murata, "Fixpoint Semantics for a Petri Net Model of Definite Clause Logic Programs," Technical Report No. UIC-EECS-87-2, Univ. of Illinois at Chicago, Apr. 1987. Also to appear in Advances in the Theory of Computation and Computational Mathematics, vol. 1, Ablex Pub.

Index Terms:
High-level Petri nets, logic programming, visual languages, parallel execution model, Prolog, SLD-resolution, SLD-ALG-resolution, FGHC.
Citation:
John Jeffrey, Jorge Lobo, Tadao Murata, "A High-Level Petri Net for Goal-Directed Semantics of Horn Clause Logic," IEEE Transactions on Knowledge and Data Engineering, vol. 8, no. 2, pp. 241-259, April 1996, doi:10.1109/69.494164
Usage of this product signifies your acceptance of the Terms of Use.