Satisfiability Testing for Non-clausal Propositional Calculus by Using Petri Nets
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
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
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://global.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 -
English
