This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Logical Inference of Horn Clauses in Petri Net Models
June 1993 (vol. 5 no. 3)
pp. 416-425

Petri net models for the Horn clause form of propositional logic and of first-order predicate logic are studied. A net model for logical inconsistency check is proposed. Algorithms for computing T-invariants of Petri net models of logical inference systems are investigated. The algorithms are based on the idea of resolution and exploit the presence of one-literal, pure-literal, and splitting clauses to lead to faster computation. Algorithms for computing T-invariants of high-level Petri net (HLPN) models of predicate logic are presented.

[1] K. R. Apt and M. H. van Emden, "Contributions to the theory of logic programming,"JACM, vol. 29, pp. 841-862, 1982.
[2] C. L. Chang and R. C. T. Lee,Symbolic Logic and Mechanical Theorem Proving. New York: Academic, 1973.
[3] M. Davis and H. Putnam, "A computing procedure for quantification theory,"J. Ass. Comput. Mach., vol. 7, no. 3, pp. 201-215, 1960.
[4] H. J. Genrich, "Predicate/transition nets," inPetri Nets Central Models and Their Properties, W. Brauer, Ed. Berlin, Heidelberg, New York: Springer-Verlag, 1987, pp. 207-247.
[5] H. J. Genrich, K. Lautenbach, and P. S. Thiagarajan, "Elements of general net theory," inLecture Notes in Computer Sci., vol. 84, 1980, pp. 21-163.
[6] A. Giordana and L. Saitta, "Modeling production rules by means of predicate transition networks,"Inform. Sci., vol. 35, pp. 1-41, 1985.
[7] C. Gunter and V. Gehlot, "Nets as tensor theories,"Proc. 10th Int. Conf. Applications and Theory of Petri Nets, 1989.
[8] J. N. Hooker, "A quantitative approach to logical inference,"Decision Support Syst., vol 4, no 1, 1988.
[9] R.G. Jeroslow and J. Wang, "Solving propositional satisfiability problems," Working Paper, Georgia Inst. Technol., Atlanta 1987.
[10] K. Jensen, "Colored Petri nets," inAdvances in Petri Nets(LNCS 254). New York: Springer-Verlag, 1987, pp. 248-299.
[11] R. Kowalski,Logic for Problem Solving. New York: North-Holland, 1979.
[12] K. Lautenbach, "On logical and linear dependencies," St. Augustin, Germany, GMD Rep. 147, 1985.
[13] C. Lin and D. C. Marinescu, " On the analysis of stochastic high level petri net models,"Microelectronics and Reliability, vol. 31, no. 4, pp. 747-767, 1991.
[14] D.C. Marinescu, M. Beaven, and R. Stansifer, "A parallel algorithm for computing invariants of Petri net models," inProc. Petri Nets and Performance Models, 1991, pp. 136-143.
[15] J. Martinez and M. Silva, "A simple and fast algorithm to obtain all invariants of a generalised Petri net,"Second European Workshop on Application and Theory of Petri Nets, 1982, pp. 301-310.
[16] T. Murata and K. Matsuyama, "Inconsistency check of a set of clauses using Petri net reductions," The Franklin Institute, 1988.
[17] T. Murata and D. Zhang, "A predicate-transition net model for parallel interpretation of logic programs,"IEEE Trans. Software Eng., vol. 14, no. 4, pp. 481-497, Apr. 1988.
[18] N. Nilsson,Principles of Artificial Intelligence. Palo Alto, CA: Tioga, 1980.
[19] J. Pearl, "Fusion, propagation, and structuring in belief networks,"Artif. Intell., vol. 29, no. 3, pp. 241-288, 1986.
[20] G. Peterka and T. Murata, "Proof procedure and answer extraction in Petri net model of logic programs,"IEEE Trans. Software Eng., vol. 15, pp. 209-217, 1989.
[21] W. Reisig, "Petri nets: An introduction," inEATCS Monographs on Theoretical Computer Science. New York: Springer-Verlag, 1985.
[22] A. Sinachopoulos, "Derivation of a contradiction by resolution using Petri nets."Petri Net Newsletter, vol. 26, pp. 16-29, 1989.

Index Terms:
logical inference; Horn clauses; Petri net models; propositional logic; first-order predicate logic; net model; logical inconsistency check; T-invariants; resolution; one-literal; pure-literal; splitting clauses; Horn clauses; inference mechanisms; Petri nets
Citation:
C. Lin, A. Chaudhury, A. Whinston, D.C. Marinescu, "Logical Inference of Horn Clauses in Petri Net Models," IEEE Transactions on Knowledge and Data Engineering, vol. 5, no. 3, pp. 416-425, June 1993, doi:10.1109/69.224194
Usage of this product signifies your acceptance of the Terms of Use.