充足可能性問題の代数化 : 同次証明方程式による判定法
スポンサーリンク
概要
- 論文の詳細を見る
筆者は推論の代数化によって、充足可能性問題がある加群における一次方程式(証明方程式)の可解問題に変換できることをすでに示し、これを代数的証明原理と名付けた。この代数的証明原理が成立するための十分条件として、充足可能性の判定対象である節集合に対して陰Horn条件が存在していた。その後この代数的証明原理がFarkasの定理に似ていることからその関係を追及した結果、代数的証明原理を再証明し、かつその成立条件としていくつかの類似の条件とそれらの関係が明らかになった。さらにそれらを整理すると、同次一次方程式(同次証明方程式)の解の様子から充足可能性を判定する方法としてまとめられる。そこでここではこれらの結果について概要を報告する。なお次の記号を用いる。n…節集合の節の個数,λ…命題記号の個数,Z…整数の全体,I={1,2,…,n},K={1,2,…,λ},K_o=K∪{0},J={1,2,…,m},(m…任意の数)。
- 一般社団法人情報処理学会の論文
- 1990-03-14
著者
関連論文
- 一階述語論理における代数的証明原理
- 推論加群系と自動証明への応用(計算モデルと計算の複雑さに関する研究)
- 拡張された推論加群系とその代数
- 一階述語論理における推論と充足の代数化
- 充足可能性問題の代数化 : 同次証明方程式による判定法