Logical inference of clauses based on Petri net models

This paper extends the logical inference of Horn clauses in Petri net models to cover a large class of non-Horn clauses. Based on four-valued logic and the conflict transition concept, we show how the Petri net model for this class of non-Horn clauses can be constructed. The clause inference is solved by the T-invariant method or the fixpoint of markings. Both forward and backward inference can be used in our:model. It is further shown that these techniques are efficient for the common classes of monotonic reasoning. (C) 1998 John Wiley & Sons, Inc.