命題論理における推論と充足の代数化

• Item type: SIG Technical Reports(1)
• 公開日: 1992-07-17
• タイトル: 命題論理における推論と充足の代数化
• タイトル / 言語: en
• タイトル: Algebraization of inference and satisfiability in Propositional Logic
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: (株)東芝総合研究所
• 著者所属(英): en
• 著者所属(英): Information Systems Laboratory, Toshiba Research and Development Center.
• 著者名: 山崎, 勇
• 著者名(英): Isamu, Yamazaki
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 命題論理における節集合の充足可能性問題を考える。加法が推論に相当する加群（推論加群）を定義すると、陰Horn条件を満たす節集合の充足可能性問題は、推論加群の上での一次方程式（証明方程式）に非負の解があるかどうかという可解問題に変換できる[1]。この代数的証明原理と線形不等式論のFarkasの定理[5]とはその言明がよく似ている。そこで、推論だけでなく割当てと充足をも代数化し、離散的Farkasの定理と関係をつけることで、代数的証明原理における陰Horn条件を必要十分条件である一般Horn条件にまで拡大できることを明らかにした。証明方程式は多項式時間で解けるから、この一般Horn条件を満たす節集合の充足可能性は多項式時間で解ける。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: By constructing a deductive module D, where addition corresponds to a kind of deduction, we can prove that a set of hidden Horn clauses S is unsatisfiable if and only if the linear Proving Equation derived from S has a nonnegative integral solution. This fact, named 'the Algebraic Proving Principle', is analogous to the Farkas's theorem on linear in equality systems. In order to reveal the relation between them, we have algebraized the interpretation and the satisfiability, as well as the deduction. Furthermore, using discrete Farkas's theorem, we have derived the weakest condition to S, named 'generalized Horn condition', under which the Algebraic Proving Principle still holds.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN1009593X
• 書誌情報: 情報処理学会研究報告アルゴリズム（AL）; 巻 1992, 号 58(1992-AL-028), p. 1-8, 発行日 1992-07-17
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会