導出計算とその応用
2009se131 小松寛
指導教員：佐々木克巳

1はじめに本研究の目的は，導出計算という形式手法を用いて，実際に問題を解けるようになることである．具体的には，[1]に従って，導出計算を理解すること，および，実際の具体的な問題を解くことを行った．
卒業論文では，最初に導出計算で必要な概念，すなわち，命題論理の論理式，トートロジー，論理和標準形，述語論理の論理式とその恒真性，存在冠頭論理式，スコーレム標準形について述べた．次に，導出計算の基礎である命題論理の導出計算 R0 を述べ，述語論理に対する導出計算 R1 ，単一化を用いる導出計算 R2 へと拡張した．最後に，実際に問題に適用し，その問題の解を導いた．
本稿では，R2 およびそれに必要な概念を導入し，[1] で紹介されている実際の問題を，[1] の解とは双対な形で解く．

2

述語論理と標準形

この節では，述語論理と，いくつかの標準形を，[1] にしたがって導入する．
まず，述語論理を導入する．ここで用いる述語論理の言語は以下である．

1) 論理結合子∧，∨ ，⊃ ，¬2) 量化記号∀，∃3) 対象変数x，y ，z ，· · ·4) 対象定数c，d，· · ·5) 関数記号f ，g ，· · ·6) 述語記号P ，Q，· · ·7) 補助記号(，)，，(コンマ)
原子論理式，リテラル，論理式はこれらからふつうの方法で定義する．その詳細は [1] にしたがう．これらの論理式の恒真性および，同値性の定義も [1] にしたがう．二つの論理式 A と B が同値であることを A ≡ B と表す．
次に，論理和標準形，冠頭論理式，存在冠頭論理式を導入する．

理式という．
定義 2.7 存在冠頭論理式
現れる量化記号がすべて ∃ である冠頭論理式を存在冠頭論理式という．
補助定理 2.2
任意の論理式 A に対し，ある存在冠頭論理式 A+ が存在して，A が恒真のとき，またそのときに限り A+ は恒真になる．
証明 上の A+ は次のように求める．
0
まず，A と同値な冠頭論理式 A を次の同値性などを用いて求める．
∀xB ∨ C ≡ ∀x(B ∨ C)(C に x は自由に現れない）∀x¬B ≡ ¬∃xB
0
次に，A が恒真であることと，A+ が恒真であることとが同値な存在冠頭論理式 A+ を求める．
0
A がすでに存在冠頭論理式になっている場合には A+00として A をとる．A が存在冠頭論理式でないとすると，
0A は(1)∃x1 · · · ∃xm ∀yCの形をしている．ただし m ≥ 0 で，C は冠頭論理式とする．このとき，新しく m 変数関数記号 f を導入し，論理式(2)∃x1 · · · ∃xm (C[f (x1 , · · · , xm )/y])を作る．(m = 0 の場合には新しく定数記号 C をとり，(2) の f (x1 , · · · , xm ) の代わりに C をとる)．
(2) の論理式が存在冠頭論理式ならば，この論理式を A+とする．そうでなければ，(2) に対して (1) に対して行ったものと同じ操作を行う．(1) から (2) を作る操作により全称記号 ∀ の数は一つ減るから，この操作を何回か繰り返すことにより存在冠頭論理式が得られる．それを A+とする．

3

R2 の導出図

この節では，R2 の導出図と，そのために必要な概念を導入する．まず，節，空節，節集合，相補的，導出節，導出原理を次のように定める．
節 リテラルの有限集合を節という．

空節 空の節を空節といい，□と表す．
定義 2.5 論理和標準形
節集合 節の有限集合を節集合という．
Aij（1 ≦ i ≦ m, 1 ≦ j ≦ ni ）をリテラルとするとき，nm
相補的 原子論理式 A に対して，A を (¬A を），¬A の∨ ∧i
Aij の形の論理式を論理和標準形という．
(A の）相補的なリテラルといい，(¬A)∗ と (A∗ と）
i=1 j=1表す．
補助定理 2.1
量化記号を含まない任意の論理式 A に対して，A と同 導出節 二つの節 C1 と C2 があり，C1 にリテラル A が属し，C2 に相補的な A∗ が属しているとする．このと値な論理和標準形の論理式が存在する．
きの節（C1 -A) ∪ (C2 -A∗ ) を導出節という．
定義 2.6 冠頭論理式

Q1 , · · · , Qn を ∀ または ∃，B を量化記号を含まない論理式としたとき，Q1 x1 · · · Qn xn B の形の論理式を冠頭論導出原理 二つの節からその導出節を作り出す操作のこと
を導出原理という．

F (x, y)，L(x, y) はそれぞれ「x は y と友達である」，「x は次に，単一化代入を導入する．{E1 , · · · , En } を表現の集 y が好きである」を表すものとする．いま(1) イチロウは男の子でケイコは女の子である．
合とする．代入 θ が {E1 , · · · , En } の単一化代入 (uniﬁer)(2) ジュンの友達はみな背が高い．
であるとは，E1 θ = E2 θ = … = En θ が成り立つこと(3) ヒロシは背が高い女の子は誰でも好きだ．とする．また，集合 {E1 , · · · , En } に対し単一化代入が(4) イチロウとケイコはジュンの友達である．
存在するときには，この集合は単一化可能であるという．と仮定する．目標はそしてさらに，{E1 , · · · , En } が単一化可能のとき，µ が(5) ジュンの友達のうち，ヒロシが好きな人がいる．
{E1 , · · · , En } の単一化代入であり，さらに {E1 , · · · , En }のどんな単一化代入 θ をとってもある代入 σ をとると が正しいか．そして，それが正しいときに，それは誰か？
θ = µ ◦ σ の形に表せるのであれば，µ を最も一般的な単 という問に答えることとする．
一化代入 (mgu) という．ただし，θ = µ ◦ σ は，二つの代 解（ここでは [1] の解と双対な形を述べる）
上記の (1) から (5) を題意に基づき論理式で表すと入 µ と σ を順に適用した結果を表すとする．
(1)B(i) ∧ G(k)さて，導出計算 R2 における，節集合 S から節 C に到
(2)∀x(F (j, x) → T (x))
る導出図は次のように定義される．
(3)∀y(T (y) ∧ G(y) → L(h, y))
定義 3.1(4)F (j, i) ∧ F (j, k)
節集合 S から節 C に到る R2 の導出図を次のように定(5)∃z(L(h, z) ∧ F (j, z))
義する．のようになる．
1) 節 C が S に属す場合，C だけからなる図は S から C
まず，問の前半は，に到る導出図である．
((1) ∧ (2) ∧ (3) ∧ (4)) ⊃ (5) が恒真(∗)
かどうかを調べればよい．補助定理
2.1
，補助定理
2.2，定2) S から節 C1 および C2 に到る導出図 D1 およびD2 が与えられているとする．また µ1 と µ2 はともに 理 3.2 より，量化記号を含まない論理式 A と節 S が存在
変数を変数でおきかえる代入で，C1 µ1 と C2 µ2 に共 して，((1) ∧ (2) ∧ (3) ∧ (4)) ⊃ (5) が恒真
通な変数は現れないものとする．ここで C1 µ1 に属す⇔ ∃x1 · · · ∃xn A が恒真るリテラルのうち A1 , · · · , Am (m ≥ 1) と C2 µ2 に属⇔ ∃x1 · · · ∃xn d(S) が恒真するリテラルのうち B1 , · · · , Bn (n ≥ 1) に対し集合∗∗⇔ R2 で S から空節□が導出可能{A1 , · · · , Am , B1 , · · · , Bn } が単一化可能であり，そのmgu が θ であるとする．さらに節 C を C = ((C1 µ1 − がいえる．よって，上の条件を満たす S を求めて，S から{A1 , · · · , Am }) ∪ (C2 µ2 − {B1 , · · · , Bn }))θ により定め 空節□を導く導出図を作成できるかを調べればよい．まる．このとき次のようにして得られる図は S から C に到 ず S を求める．
((1) ∧ (2) ∧ (3) ∧ (4)) ⊃ (5)る導出図である．
≡¬((1) ∧ (2) ∧ (3) ∧ (4)) ∨ (5)≡¬(1) ∨ ¬(2) ∨ ¬(3) ∨ ¬(4) ∨ (5)D1 D2≡¬B(i) ∨ ¬G(k) ∨ ∃x(F (j, x) ∧ ¬T (x))
C1 C2∨∃y(T (y) ∧ G(y) ∧ ¬L(h, y)) ∨ ¬F (j, i) ∨ ¬F (j, k)＼／∨∃z(L(h, z) ∧ F (j, z))≡ ∃x∃y∃z(¬B(i) ∨ ¬G(k) ∨ (F (j, x) ∧ ¬T (x))
C∨(T (y) ∧ G(y) ∧ ¬L(h, y)) ∨ ¬F (j, i)∨¬F (j, k) ∨ (L(h, z) ∧ F (j, z)))定理 3.2（述語論理の導出計算 R2 の完全性）
よって，S を空でない任意の節集合とする．また，x1 , · · · , xn
S = {{¬B(i)}, {¬G(k)}, {F (j, x), ¬T (x)},を S に現れる変数全体の集合とする．このとき，論理式{T (y), G(y), ¬L(h, y)}, {¬F (j, i)},∃x1 · · · ∃xn d(S) が恒真になるための必要十分条件は R2{¬F (j, k)}, {L(h, z), F (j, z)}}で S から空節が導出可能となることである．ただし，節この S から□に到る導出図を作成することができる（本集合 S = {C1 , · · · , Cm } に対して，稿では省略する）．よって，(∗) がいえるので，問の前半
d(S) = (∧C1 ) ∨ · · · ∨ (∧Cm )は「正しい」となる．と定める．d(S) は論理和標準形の論理式である．
問の後半は，(5) の論理式から，省略した導出図における z へ代入されたものを考えればよい．その導出図では，4 問題
z に k が代入されているので，ケイコが問の後半に対す
この節では，導出計算 R2 を，実際に問題に適用し，そ る答えである．の問題の解を導く．以下の問は [1] の例である．
問 h, i, j, k はそれぞれヒロシ，イチロウ，ジュン，ケイ 参考文献
コを表す．B(x)，G(x)，T (x) はそれぞれ「x は男のであ [1] 小野寛晰：『情報科学における論理』．日本評論社，東る」，「x は女の子である」，「x は背が高い」を表し，また京，1994．