Satisfiability Testing for Non-clausal Propositional Calculus by Using Petri Nets

Won Ho CHUNG  Ha Ryoung OH  Myunghwan KIM  

Publication
IEICE TRANSACTIONS (1976-1990)   Vol.E73   No.4   pp.539-544
Publication Date: 1990/04/25
Online ISSN: 
DOI: 
Print ISSN: 0000-0000
Type of Manuscript: PAPER
Category: Graphs and Networks
Keyword: 


Full Text: PDF(530.7KB)>>
Buy this Article




Summary: 
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.