一階述語論理における推論と充足の代数化
スポンサーリンク
概要
- 論文の詳細を見る
非負一次結合が演繹推論に相当するような加群を定義すると,節集合の充足可能性問題は,この加群の元を係数とし,加群の係数環の元を未知数とする一次方程式(証明方程式)に非負の解があるかどうかという問題と,陰Horn条件と名付けた十分条件のもとで等価であることは,代数的証明原理としてすでに導かれている.本論文では割当てに相当する加群を導入し,充足を代数化することによってFarkasの定理を代数的証明原理と関係づけ,上記の等価性が成り立つための必要十分条件として一般Horn条件を明らかにした.これらを通して一階述語論理での議論と問題解決に加群を用い得ることを示し,その土台となる1つの代数系を提案した.
- 日本ソフトウェア科学会の論文
- 1995-03-15
著者
関連論文
- 一階述語論理における代数的証明原理
- 推論加群系と自動証明への応用(計算モデルと計算の複雑さに関する研究)
- 拡張された推論加群系とその代数
- 一階述語論理における推論と充足の代数化
- 充足可能性問題の代数化 : 同次証明方程式による判定法