■
プロットしました。
Maxcompをインストールした
Maxcompはknuth-bendixのアルゴリズムないしmkbtt(多重完備化)とは別の完備化アルゴリズムおよび,それのデモプログラムです.JAISTで公開されています.
http://www.jaist.ac.jp/project/maxcomp/
個人的に完備化したい項書き換え系があったのでインストールしました.
オーダーはlpo,rpo,kboが指定できます.ただしこれについては専門的な知識が必要です.詳しい説明はTerm Rewriting and All Thatを読むなどして調べてください.
Ubuntuで動作します.今回はUbuntu 16.04上で作業しました.
1. Yices 1.0.40をインストールする
MaxcompはYices 1.0.40を利用しています.Yicesの現行バージョンは2系列なので,最新のバージョンをインストールしないよう注意してください.
http://yices.csl.sri.com/old/download-yices1-full.shtmlの「Yices with GMP dynamically linked」から「 Linux/x86_64 (64bit AMD/Intel and compatible)」を選択しDLしてください.
DLしたyices-1.0.40-x86_64-unknown-linux-gnu.tar.gzを展開したあと,libディレクトリに移動しaファイルとsoファイルをインストールします.
$ tar xvf yices-1.0.40-x86_64-unknown-linux-gnu.tar.gz
$ cd ./yices-2.5.1/lib
$ sudo install ./libyices.a ./libyices.so /usr/local/lib
2. libgmp10のインストール
こちらは公式にある手順通りに行います.
$ sudo apt-get install libgmp10 libgmp10-dev
$ sudo /sbin/ldconfig -v
3. maxcompのページからBinary Package for Ubuntu 12.04 64bitをDLする
Binary Packageが公式で公開されています.
http://www.jaist.ac.jp/project/maxcomp/
4. 3でDLしたPackageをdpkgでインストールする
$ sudo dpkg -i ./maxcomp_1.0-1_amd64.deb
インストールする手順は以上です.これでTermからmaxcompが動かせるようになっているはず.
動かしてみる
成功例として群を完備化してみます.
$ vim group.trs
(VAR x y z) (RULES *(*(x, y), z) -> *(x, *(y, z)) *(x, e) -> x *(x, i(x)) -> e )
$ maxcomp -s lpo group.trs
EQUATIONS: times(times(x,y),z) = times(x,times(y,z)) times(x,e()) = x times(x,i(x)) = e() COMPLETE TRS: RULES: times(times(x,y),z) -> times(x,times(y,z)) times(x,e()) -> x times(x,i(x)) -> e() times(e(),x) -> x i(i(x)) -> x times(i(x),x) -> e() times(i(x),times(x,y)) -> y times(y,times(i(y),x)) -> x i(e()) -> e() i(times(y,x)) -> times(i(x),i(y)) SUCCESS Search time: 0.05 seconds
COMPLETE TRSとSUCCESSのメッセージが表示されれば成功です.
次に失敗例として環を完備化してみます.
$ vim ring.trs
(VAR x y z) (RULES +(+(x, y), z) -> +(x, +(y, z)) +(x, 0) -> x +(x, -(x)) -> 0 *(*(x, y), z) -> *(x, *(y, z)) *(x, 1) -> x *(x, /(x)) -> 1 *(x, +(y, z)) -> +(*(x, y), *(x, z)) *(x, 0) -> 0 )
$ maxcomp -s lpo ring.trs
EQUATIONS: plus(plus(x,y),z) = plus(x,plus(y,z)) plus(x,0()) = x plus(x,minus(x)) = 0() times(times(x,y),z) = times(x,times(y,z)) times(x,1()) = x times(x,slash(x)) = 1() times(x,plus(y,z)) = plus(times(x,y),times(x,z)) times(x,0()) = 0() Fatal error: exception Maxcomp.Fail("I'm giving up")
"I'm giving up"と表示されれば完備化の失敗です.maxcomp + (lpo | rpo | kbo)では完備化できなかったことを意味します.
破壊される工学
画像は自由に転載していただいて構いません.
古典論理の推論規則から3値論理の演算を補完する
はじめに2値論理
通常の論理学は論理演算fに真(True),偽(False)いずれかの引数を2つ取り,同様に真偽のいずれかの値を1つ返します.
以下に2値論理におけるEqual, NotEqual, And, Or, Implication, Notを表としてまとめます.左から左辺,右辺,評価結果と並んでいます.
Equal : x = y | ||
---|---|---|
T | T | T |
T | F | F |
F | T | F |
F | F | T |
NotEqual : x /= y | ||
---|---|---|
T | T | F |
T | F | T |
F | T | T |
F | F | F |
And : x ∧ y | ||
---|---|---|
T | T | T |
T | F | F |
F | T | F |
F | F | F |
And : x ∨ y | ||
---|---|---|
T | T | T |
T | F | T |
F | T | T |
F | F | F |
Impl : x ⇒ y | ||
---|---|---|
T | T | T |
T | F | F |
F | T | T |
F | F | T |
Not : ¬x | |
---|---|
T | F |
F | T |
見やすいようにひとつのテーブルにまとめます.
LHS | RHS | ∧ | ∨ | ⇒ | ¬ |
---|---|---|---|---|---|
T | T | T | T | T | F |
T | F | F | T | F | |
F | T | F | T | T | T |
F | F | F | F | T |
含意(Implication)についてはAndとNotを使った表現方法があり,以下と同値です.
また,古典論理に限ってド・モルガンの法則を使って次のように変形できます.
2値論理における推論規則
推論とは「AならばB」のことで,推論規則とはImplicationの形で与えられる論理式の真偽を判定するための規則です.と書きます.ただしここでは論理演算Implicationとは区別し,演算子の優先順位を1つ下げます.
古典論理における推論規則には以下の11があります.また,詳細は後述しますが,3値論理を導入する際に古典論理との整合性を保つためにこの推論規則から3値目の論理値の振る舞いを制約としてある程度決定することができます.
前件肯定:
後件肯定:
否定導入:
二重否定の除去:
二重否定の導入:
選言三段論法:
仮言三段論法:
導出:
普遍例化:
存在汎化:
後件肯定:
推論規則から3値目の値の振る舞いを決定する
前置きが長くなってしまいました.このエントリで本当に述べたかったことはここの節からです.
3値目の値をUとするならば,当然,その値の推論規則による振る舞いが決定されていなければなりません.そしてその振る舞いは古典論理の拡張であるならば自由に決定できるものではなく,制約を満たした上で決定されます.
その制約を得てみましょう.アルゴリズムは各推論規則に対し自由変数にUを代入して変数を消去することによって進行します.以下の通りです.
1. 推論において,左辺に出現する自由変数にUを代入したときにRHSをTrueにする式の形から論理演算を決定する.
2. 推論において,AをTrueにする変数の組み合わせがBへの制約条件となり,B中に存在する自由変数にUを代入する.そのあとの方針は1と同じ.
前件肯定: 前件肯定: P, P -> Q |- Q より T, T -> U |- U よって T -> U = T 後件否定: ¬Q, P -> Q |- ¬P より ¬F, U -> F |- ¬U よって U -> F = T 否定導入: P -> F |- ¬P より U -> F |- ¬U よって U -> F = T 二重否定の除去: ¬¬P |- P より ¬U = x1 ¬x1 = x2 x2 -> U = T より ¬U = F ならば ¬U = F = x1 ¬F = T = x2 T -> U = T よって ¬U = F -- 3 二重否定の導入: P |- ¬¬P よって ¬U = F U -> ¬¬U = U -> ¬F = U -> T = T 選言三段論法: P ∨ Q, ¬P |- Q より F ∨ U, ¬F |- U よって F ∨ U = T T -> U = T 仮言三段論法: P -> Q, Q -> R |- P -> R より U -> Q, Q -> R |- U -> R より U -> T, T -> T |- U -> T よって U -> T = T P -> U, U -> R |- P -> R より P -> U, U -> T |- P -> T より T -> U, U -> T |- T -> T F -> U, U -> T |- F -> T U -> U, U -> T |- U -> T よって U -> U = T U -> T = T P -> Q, Q -> U |- P -> U より T -> T, T -> U |- T -> U T -> U, U -> U |- T -> U F -> T, T -> U |- F -> U F -> F, F -> U |- F -> U F -> U, U -> U |- F -> U U -> T, T -> U |- U -> U U -> F, F -> U |- U -> U U -> U, U -> U |- U -> U よって F -> U = T 導出: L ∨ P, ¬L ∨ Q |- P ∨ Q より T ∨ T, ¬T ∨ U |- T ∨ U よって F ∨ U = T T ∨ U = T F ∨ T, ¬F ∨ U |- T ∨ U よって T ∨ U = T T ∨ U, ¬T ∨ T |- U ∨ T よって U ∨ T = T F ∨ U, ¬F ∨ T |- U ∨ T よって F ∨ U = T F ∨ U, ¬F ∨ F |- U ∨ F よって U ∨ F = T 後件肯定: Q, P -> Q |- P より T, U -> T |- U よって U -> T = T T -> U = T
以上の手続きから3値目の値に対する論理演算の一部が得られました.
前件肯定より
後件否定より
二重否定の除去より
二重否定の導入より
選言三段論法より
仮言三段論法より
仮言三段論法より
導出より
実際には,古典論理からの互換性が必須でないため,論理演算の妥当性を優先するならば推論規則をいくつか棄却して制約条件を得なければなりません.