PROOF OF UNSATISFIABILITY OF ATOM SETS BASED ON COMPUTATION BY EQUIVALENT TRANSFORMATION RULES

• Miura, Katsunori

• Akama, Kiyoshi

• Koike, Hidekatsu

• Mabuchi, Hiroshi

抄録

Equivalent Transformation (ET) rules can be used to construct correct sequential and parallel programs, as they are inherently correct. One important method for making ET rules uses logical formulas. Among logical formulas, unsatisfiable conjunctions of finite 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 programs. This paper proposes a method of proving unsatisfiability 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 find a new atom set based on subset relation or inductive structure. Since our proposed method incorporates search based on subset and inductive relations, it can be used to prove unsatisfiability of various atom sets that cannot be proven by conventional methods.

収録刊行物

• International Journal of Innovative Computing, Information and Control

  International Journal of Innovative Computing, Information and Control 9 (11), 4419-4430, 2013-11

  ICIC International

キーワード

• Unsatisability
• Proof
• Equivalent transformation rule
• Induction
• メディア・コミュニケーション

詳細情報

• CRID: 1050282677810357376
• NII論文ID: 120005649801
• NII書誌ID: AA12218449
• ISSN: 13494198
• Web Site: http://hdl.handle.net/10252/00005828
• Web Site: https://kitami-it.repo.nii.ac.jp/records/7952
• 本文言語コード: en
• 資料種別: journal article
• データソース種別:
  • IRDB
  • CiNii Articles
  • KAKEN