Petri net models and efficient T-invariant analysis for logical inference of clauses

This paper presents the Petri net representation of a set of nonHorn clauses for logical inference. The paper proposes an algorithm for hierarchically finding the T-invariants of a large scale Petri net model of a clause system. This algorithm is based on the idea of resolution and exploits the presence of one-literal, pure-literal and splitting clauses for faster computation. The splitting rule is important for decomposition of a large scale system and parallel computation of T-invariants. Two inference techniques (forward inference and backward inference) are given to solve the clause inference