A Petri Net Approach for Logical Inference of Clauses

Abstract

Logical inference of clauses has been an important technique in automated reasoning. The process of inference determines whether a given clause is implied by a collection of clauses. Petri nets have been a popular formalism for modelling the behavior of complex systems. A large volume of techniques have been developed to analyze Petri net models and derive conclusions about the logical behavior of systems. The computation of the T-invariants for Petri net models enable us to study their logical properties. Mapping between Horn clauses and Petri nets have been proposed in the literature. In this paper, we survey the mapping techniques proposed in the literature. We also show how this mapping can be extended to non Horn clauses.

Indexing terms:

• Petri nets
• Logical inference
• Clauses
• Automated reasoning
• Horn clauses