LOGICAL INFERENCE OF HORN CLAUSES IN PETRI NET MODELS

This paper studies Petri net models for the Horn clause form of propositional logic and of first order predicate logic. A net model for logical inconsistency check is pro-posed. Algorithms for computing T·invariants of Petri net models of logical inference systems are investigated. The algorithms are ba8ed 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 models of predicate logic are presented