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

Won Ho CHUNG; Ha Ryoung OH; Myunghwan KIM

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

Won Ho CHUNG, Ha Ryoung OH, Myunghwan KIM

Full Text Views

0

Share
Cite this

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.

Publication: IEICE TRANSACTIONS on transactions Vol.E73-E No.4 pp.539-544

Publication Date: 1990/04/25

Publicized

Online ISSN

DOI

Type of Manuscript: PAPER

Category: Graphs and Networks

Authors

Won Ho CHUNG
Ha Ryoung OH
Myunghwan KIM

Keyword

Cite this

Copy

Won Ho CHUNG, Ha Ryoung OH, Myunghwan KIM, "Satisfiability Testing for Non-clausal Propositional Calculus by Using Petri Nets" in IEICE TRANSACTIONS on transactions, vol. E73-E, no. 4, pp. 539-544, April 1990, doi: .
Abstract: 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.
URL: https://globals.ieice.org/en_transactions/transactions/10.1587/e73-e_4_539/_p

Copy

@ARTICLE{e73-e_4_539,
author={Won Ho CHUNG, Ha Ryoung OH, Myunghwan KIM, },
journal={IEICE TRANSACTIONS on transactions},
title={Satisfiability Testing for Non-clausal Propositional Calculus by Using Petri Nets},
year={1990},
volume={E73-E},
number={4},
pages={539-544},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={April},}

Copy

TY - JOUR
TI - Satisfiability Testing for Non-clausal Propositional Calculus by Using Petri Nets
T2 - IEICE TRANSACTIONS on transactions
SP - 539
EP - 544
AU - Won Ho CHUNG
AU - Ha Ryoung OH
AU - Myunghwan KIM
PY - 1990
DO -
JO - IEICE TRANSACTIONS on transactions
SN -
VL - E73-E
IS - 4
JA - IEICE TRANSACTIONS on transactions
Y1 - April 1990
AB - 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.
ER -