2024-03-29T13:34:22Z
https://kitami-it.repo.nii.ac.jp/oai
oai:kitami-it.repo.nii.ac.jp:00007952
2022-12-13T02:19:39Z
1:87
PROOF OF UNSATISFIABILITY OF ATOM SETS BASED ON COMPUTATION BY EQUIVALENT TRANSFORMATION RULES
Miura, Katsunori
Akama, Kiyoshi
Koike, Hidekatsu
Mabuchi, Hiroshi
c 2013 ICIC International
Unsatisability
Proof
Equivalent transformation rule
Induction
Equivalent Transformation (ET) rules can be used to construct correct se-
quential and parallel programs, as they are inherently correct. One important method
for making ET rules uses logical formulas. Among logical formulas, unsatis able con-
junctions of nite atoms, each of which is represented by an atom set in this paper, are
especially useful for making many ET rules that are used for constructing efficient pro-
grams. This paper proposes a method of proving unsatis ability of an atom set based on
computation by ET rules. The proposed method is recursive, in the sense that, during
proving the given atom set, it may nd a new atom set based on subset relation or in-
ductive structure. Since our proposed method incorporates search based on subset and
inductive relations, it can be used to prove unsatis ability of various atom sets that can-
not be proven by conventional methods.
ICIC International
2013-11
eng
journal article
VoR
https://kitami-it.repo.nii.ac.jp/records/7952
International Journal of Innovative Computing, Information and Control
9
11
4419
4430
https://kitami-it.repo.nii.ac.jp/record/7952/files/2013.11_Proof of Unsatisfiability of Atom Sets based on Computation by Equivalent Transformation Rules.pdf
application/pdf
146.7 kB
2016-11-22