This paper studies Petri net models for the Horn clause form of propositional logic. Since finding the T-invariants of Petri net models of logical inference is the key step, the paper investigates the algorithms for computing such invariants. These are based on the idea of resolution, and exploit the presence of one-literal, pure -literal and splitting clauses to lead to faster computation.