A Petri net with negative tokens and its application automated reasoning
Tadao Murata, Hirozumi Yamaguchi · 2002
A modified Petri-net model is introduced with negative tokens for automated reasoning programs. In this model, Horn and non-Horn clauses are represented by transitions and predicate symbols by places. UR-resolution is simulated by either forward or background firing of a transition and demodulation by a transition which rewrites tokens. This model is intended to provide a means to analyze structural properties of automated reasoning programs and an operational semantics of programs.>