For Full-Text 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 Non-clausal Propositional Calculus by Using Petri Nets
Won Ho CHUNG Ha Ryoung OH Myunghwan KIM
IEICE TRANSACTIONS (1976-1990)
Publication Date: 1990/04/25
Print ISSN: 0000-0000
Type of Manuscript: PAPER
Category: Graphs and Networks
Full Text: PDF(530.7KB)>>
Petri net based satisfiability testing for non-clausal propositional calculus is presented. Every formula in propositional calculus is hierarchically represented by an acyclic free-choice 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 non-clausal form can be tested by obtaining reachable firing set of the complete logic Petri net corresponding to the formula under the maximum firing rule.