拡張された推論加群系とその代数
スポンサーリンク
概要
- 論文の詳細を見る
論理を線形代数に近い代数系の上で表すことにより論理の問題に新しい視点をあたえることを目的として,すでに推論加群Dとその係数環R,および割当加群Uから成る推論加群系を定義し,いくつかの論理的な事項をこれらの加群系の上で表現し直した.例えば,充足は内積の非負性と,モデルの全体は双対錐と,論理的帰結の全体は双対錐の双対錐と,推論は非負一次結合と,対応する.本論文では一歩進んで,論理上の問題解決法を推論加群系の上で表現できるようにすることを目的として,推論加群が双対加群を持つように拡張した.すなわち左単一化関数にもとづいて,推論加群Dとその係数環R,ならびに推論加群の双対加群の部分加群(事実加群Ψ)を導いた.またこの新しい推論加群系の上での代数について述べた.推論加群はねじれ加群であるが,準一次独立なる概念を導入することで線形代数に準ずる議論を行える.以上により推論加群系の上での一次方程式を,消去したい未知数の係数を0とする射影変換を構成してこれを方程式に作用させる,という消去法を実行するための土台が築かれた.これに基づき従来の充足可能性判定手順の一つである単位導出法に対応する消去法を述べ,これらの方法が一般Horn条件のもとで完全であることを導いた.
- 日本ソフトウェア科学会の論文
- 1997-03-17
著者
関連論文
- 一階述語論理における代数的証明原理
- 推論加群系と自動証明への応用(計算モデルと計算の複雑さに関する研究)
- 拡張された推論加群系とその代数
- 一階述語論理における推論と充足の代数化
- 充足可能性問題の代数化 : 同次証明方程式による判定法