This Article 
 Bibliographic References 
 Add to: 
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
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.