A propositional logic program P consisting of Horn clauses t₁, . . . ,t_n containing literals p₁, . . . ,p_m can be described by a Petri net with places p₁, . . . ,p_m and transitions t₁, . . . ,t_n. The transition p, . . . ,q :2WZ r has incoming arcs p, . . . ,q and outgoing arc r. The goal transition p, . . . ,q :2WZ has no outgoing arcs. Transition matrix A corresponding to a program P has dimension n × m with element a_ij = 0,±1 according to the sign of p_j in the clause t_i (in particular, it is zero if p_ij does not occur in t_i). The authors’ constructions are based on the following equivalence: P is contradictory if and only if there exists a T-invariant, that is, a vector X of nonnegative integers such that A^TX = 0 and the goal-coordinate x_g = 0. The paper is devoted to the extension of this approach to predicate logic programs. This requires a much more complicated technique of colored Petri nets, and even in this case the authors only treat function-free programs (which are finitely reducible to propositional programs). The authors conclude that “a general method and computational cost of finding T-invariants applicable to logic programming are unknown and suggested for further study.”