
For FullText PDF, please login, if you are a member of IEICE,
or go to Pay Per View on menu list, if you are a nonmember of IEICE.

Satisfiability Testing for Nonclausal Propositional Calculus by Using Petri Nets
Won Ho CHUNG Ha Ryoung OH Myunghwan KIM
Publication
IEICE TRANSACTIONS (19761990)
Vol.E73
No.4
pp.539544 Publication Date: 1990/04/25
Online ISSN:
DOI:
Print ISSN: 00000000 Type of Manuscript: PAPER Category: Graphs and Networks Keyword:
Full Text: PDF>>
Summary:
Petri net based satisfiability testing for nonclausal propositional calculus is presented. Every formula in propositional calculus is hierarchically represented by an acyclic freechoice Petri net called logic Petri net. Then a logic Petri net is combined with two way alternating modules, whose number depends upon the number of atoms used in the formula. It is shown that the satisfiability of a formula with nonclausal form can be tested by obtaining reachable firing set of the complete logic Petri net corresponding to the formula under the maximum firing rule.

