ソフトウェア科学特論: 命題論理の推論体系

Table of Contents

1 概要

本稿では,命題論理の推論体系について説明する.

1.1 注意

本Webページ(およびPDF)の作成には Emacs org-mode を用いており, 数式等の表示は MathJax を用いています. IEでは正しく表示されないことがあるため, Firefox, Safari等のWebブラウザでJavaScriptを有効にしてお使いください. また org-info.js を利用しており, 「m」キーをタイプするとinfoモードでの表示になります. 利用できるショートカットは「?」で表示されます.

1.2 参考文献

  • 小野寛晰著 『情報科学における論理』日本評論社,1994 (Amazon)
  • Chin-Liang Chang, Richard Char-Tung Lee "Symbolic Logic and Mechanical Theorem Proving", Academic Press, 1973 (Amazon)
  • Michael R. Genesereth and Nils J. Nilsson: "Logical Foundations of Artificial Intelligence", Morgan Kaufmann, 1987 (Amazon)
  • (上の邦訳) Genesereth,Nilsson著,古川康一訳 『人工知能基礎論』オーム社,1993 (Amazon)

2 命題論理の推論体系

ここでは,いくつかの命題論理式から別の新たな命題論理式を導き出す, すなわち別の新たな命題論理式を 推論 (inference)する方法について学ぶ.

命題論理について,形式的(記号的)に推論を行うための 推論体系 (inference system)には,以下のように様々な種類がある.

  • ヒルベルトの体系
  • 自然演繹 (ゲンツェンの体系NK)
  • シーケント計算 (ゲンツェンの体系LK)
  • 融合原理 (導出原理)

これらは,いずれも真と仮定する命題論理式の集合 \(\D\) から, 新しい命題論理式 \(A\) を論理的に推論するための体系である (シーケント計算は若干異なっている). これらの体系には,真と仮定している命題論理式や すでに導き出された命題論理式から, 新たな命題を導き出すための 推論規則 (inference rule)が備わっている.

3 推論体系LK

1934年にゲンツェン (Gerhard Karl Erich Gentzen)が導入した シーケント計算 (sequent calculus)の推論体系では, 推論規則の操作対象は命題論理式そのものではなく, 複数の命題論理式から構成される シーケント (sequent)と呼ばれる表現を用いる. シーケントは命題論理式間の証明可能性の関係を表している.

また,ここで学ぶ推論体系LK (logistischer klassischer Kalkül)は, 古典論理のためのシーケント計算の体系である. LKは述語論理の体系であるが,ここでは命題論理の部分について学ぶ.

3.1 シーケント

以下の表現を シーケント (sequent)と呼ぶ. \[ A_{1},A_{2},\ldots,A_{m} \lra B_{1},B_{2},\ldots,B_{n} \] ここで \(A_i\), \(B_j\) は命題論理式であり, \(m, n \ge 0\) である.

  • \(\lra\) の左辺は 前件 (antecedent)と呼ばれ, 右辺は 後件 (succedent)と呼ばれる.
  • 以下では,シーケントの一部として現れる命題論理式の0個以上の列を \(\G\), \(\D\) 等のギリシャ大文字で表す.

3.1.1 シーケントの例

\begin{eqnarray*} p, q \land r & \lra & p \lor q, r \\ & \lra & p \lor \neg q, q \\ \neg p, p \land \neg q & \lra & \end{eqnarray*}

3.1.2 シーケントの意味

シーケント \(A_{1},A_{2},\ldots,A_{m} \lra B_{1},B_{2},\ldots,B_{n}\) は, \(A_{1},A_{2},\ldots,A_{m}\) のすべてを仮定すると, \(B_{1},B_{2},\ldots,B_{n}\) のいずれかが導出できることを表現する.

すなわち \(p, q \land r \lra p \lor q, r\) は, \(p\) と \(q \land r\) を仮定すると \(p \lor q\) または \(r\) が導出できることを表し, \(\lra p \lor \neg q, q\) は, 仮定なしに \(p \lor \neg q\) または \(q\) が導出できることを表す. \(\neg p, p \land \neg q \lra\) は, 仮定 \(\neg p\) と \(p \land \neg q\) が矛盾することを表している (実際には矛盾しない). また両辺が空の \(\lra\) は, 仮定なしに矛盾することを表す. もちろん \(\lra\) が推論できる体系は望ましくない. \(\lra\) が推論できない体系は 無矛盾 であるという.

3.2 推論規則

推論規則は,横線の上が仮定のシーケント,下が結論のシーケントの形をしている. 仮定のシーケントは0個以上2個以下である.

\(\Infer{(Rule)}{\G \lra \D}{}\)  
\(\Infer{(Rule)}{\G \lra \D}{\G_1 \lra \D_1}\)
\(\Infer{(Rule)}{\G \lra \D}{\G_1 \lra \D_1 \AND \G_2 \lra \D_2}\)
  • 横線の右の (Rule) は推論規則の名称である.
  • 推論規則の下側のシーケントは下シーケントと呼ばれ, 上側のシーケントは上シーケントと呼ばれる.

3.2.1 公理規則

以下は 公理規則 (axiom rule)と呼ばれ, 仮定なしに導出されるシーケントである.

\(\Infer{(Ax)}{A \lra A}{}\)

ここで \(A\) は任意の命題論理式である点に注意する. すなわち \(A\) を任意の命題論理式で置き換えたものはすべて公理規則のシーケントである. \begin{eqnarray*} & \Infer{(Ax)}{p \land q \lra p \land q}{} \end{eqnarray*} また,後述の \({\rm (L\F)}\), \({\rm (R\T)}\) の推論規則も仮定なしにシーケントが導出される. これらは 始シーケント (initial sequent)と呼ばれる.

3.2.2 構造規則

以下は推論規則のうち 構造規則 (structural rules)と呼ばれるものである.

\(\cfrac{{\G \lra \D}}{{A,\G \lra \D}}\;{\small\rm (LW)}\)\(\cfrac{{\G \lra \D}}{{\G \lra \D,A}}\;{\small\rm (RW)}\)
\(\cfrac{{A,A,\G \lra \D}}{{A,\G \lra \D}}\;{\small\rm (LC)}\)\(\cfrac{{\G \lra \D,A,A}}{{\G \lra \D,A}}\;{\small\rm (RC)}\)
\(\cfrac{{\G,A,B,\Pi \lra \D}}{{\G,B,A,\Pi \lra \D}}\;{\small\rm (LX)}\)\(\cfrac{{\G \lra \D,A,B,\Sigma}}{{\G \lra \D,B,A,\Sigma}}\;{\small\rm (RX)}\)
  • 後述の論理結合子に関する推論規則とは異なり, シーケントの構造を変更する規則のため構造規則と呼ばれる.
  • \(\G\), \(\Pi\), \(\D\), \(\Sigma\) は0個以上の任意の命題論理式の列であり, \(A\), \(B\) は任意の命題論理式である.
  • それぞれの規則の名称の意味は以下の通りである.
    名称意味日本語の名称
    LWLeft Weakening増左
    RWRight Weakening増右
    LCLeft Contraction減左
    RCRight Contraction減右
    LXLeft Exchange換左
    RXRight Exchange換右

3.2.3 カット規則

以下は カット規則 (cut rule)と呼ばれる推論規則である.

\(\Infer{(Cut)}{\G,\Pi \lra \Delta,\Sigma}{\G \lra \D,A \AND A,\Pi \lra \Sigma}\)  

3.2.4 論理規則

以下は 論理規則 (logical rules)と呼ばれる推論規則であり, 各論理結合子に対応しており,また左と右の規則がある.

\(\Infer{(L\F)}{\F,\G \lra \D}{}\)\(\Infer{(R\F)}{\G \lra \D,\F}{\G \lra \D}\)
\(\Infer{(L\T)}{\T,\G \lra \D}{\G \lra \D}\)\(\Infer{(R\T)}{\G \lra \D,\T}{}\)
\(\cfrac{{A,\G \lra \D}}{{A\land B,\G \lra \D}}\;{\small\rm (L\land_1)}\)\(\cfrac{{\G \lra \D,A}\qquad{\G \lra \D,B}}{{\G \lra \D,A\land B}}\;{\small\rm (R\land)}\)
\(\cfrac{{B,\G \lra \D}}{{A\land B,\G \lra \D}}\;{\small\rm (L\land_2)}\)
\(\cfrac{{A,\G \lra \D}\qquad{B,\G \lra \D}}{{A\lor B,\G \lra \D}}\;{\small\rm (L\lor)}\)\(\cfrac{{\G \lra \D,A}}{{\G \lra \D,A\lor B}}\;{\small\rm (R\lor_1)}\)
\(\cfrac{{\G \lra \D,B}}{{\G \lra \D,A\lor B}}\;{\small\rm (R\lor_2)}\)
\(\cfrac{{\G \lra \D,A}\qquad{B,\Pi \lra \Sigma}}{{A\imp B,\G,\Pi \lra \D,\Sigma}}\;{\small\rm (L\imp)}\)\(\cfrac{{A,\G \lra \D,B}}{{\G \lra \D,A\imp B}}\;{\small\rm (R\imp)}\)
\(\cfrac{{\G \lra \D,A}}{{\lnot A,\G \lra \D}}\;{\small\rm (L\lnot)}\)\(\cfrac{{A,\G \lra \D}}{{\G \lra \D,\lnot A}}\;{\small\rm (R\lnot)}\)

3.3 証明図

始シーケントから始めて, 推論規則を適用したものを証明図と呼ぶ. 証明図の一番下のシーケントは 終シーケント (endsequent)と呼ばれる.

あるシーケントについて,それを終シーケントとする証明図が存在する時, そのシーケントは証明可能と呼ばれる.

3.3.1 証明図の例

以下はLKでの \(\lra A \lor \neg A\) の証明図である. \[ \Infer{(RC)}{\lra A \lor \neg A}{ \Infer{(R\lor_1)}{\lra A \lor \neg A, A \lor \neg A}{ \Infer{(RX)}{\lra A \lor \neg A, A}{ \Infer{(R\lor_2)}{\lra A, A \lor \neg A}{ \Infer{(R\neg)}{\lra A, \neg A}{ \Infer{(Ax)}{A \lra A}{} }}}}} \]

3.3.2 証明図の例

以下はLKでの \(\neg(A \land \neg B) \lra A \imp B\) の証明図である (Exchange規則の適用は省略している). \[ \Infer{(R\imp)}{\neg(A \land \neg B) \lra A \imp B}{ \Infer{(L\neg)}{A, \neg(A \land \neg B) \lra B}{ \Infer{(R\land)}{A \lra B, A \land \neg B}{ \Infer{(RW)}{A \lra B, A}{ \Infer{(Ax)}{A \lra A}{} } \AND \Infer{(R\neg)}{A \lra B, \neg B}{ \Infer{(LW)}{B, A \lra B}{ \Infer{(Ax)}{B \lra B}{} }} }}} \]

3.3.3 証明図の例

以下はLKでの \(A \imp B \lra \neg(A \land \neg B)\) の証明図である (Exchange規則の適用は省略している). \[ \Infer{(R\neg)}{A \imp B \lra \neg(A \land \neg B)}{ \Infer{(LC)}{A \land \neg B, A \imp B \lra}{ \Infer{(L\imp)}{A \land \neg B, A \land \neg B, A \imp B \lra}{ \Infer{(L\land_1)}{A \land \neg B \lra A}{ \Infer{(Ax)}{A \lra A}{} } \AND \Infer{(L\land_2)}{B, A \land \neg B \lra}{ \Infer{(L\neg)}{B, \neg B \lra}{ \Infer{(Ax)}{B \lra B}{} }} }}} \]

3.4 練習問題

  1. LKでの \(A \lra \neg \neg A\) の証明図を求めよ.
  2. LKでの \(\neg \neg A \lra A\) の証明図を求めよ.
  3. LKでの \(\neg (A \land B) \lra \neg A \lor \neg B\) の証明図を求めよ.
  4. LKでの \((A \imp B) \imp (A \imp C) \lra A \imp (B \imp C)\) の証明図を求めよ.
  5. LKでの \(A \imp \neg A \lra \neg A\) の証明図を求めよ.

3.5 LKに関する定理の例

以下は,LKに関する定理の例である.

\(\G \lra \D,A,B\) が証明可能 \(\Llra\) \(\G \lra \D,A \lor B\) が証明可能

証明
(\(\Lra\))

\[ \Infer{(RC)}{\G \lra \D, A \lor B}{ \Infer{(R\lor_1)}{\G \lra \D, A \lor B, A \lor B}{ \Infer{(R\lor_2)}{\G \lra \D, A, A \lor B}{ \G \lra \D, A, B }}} \]

(\(\Lla\))

\[ \Infer{(Cut)}{\G \lra \D, A, B}{ \G \lra \D, A \lor B \AND \Infer{(L\lor)}{A \lor B \lra A, B}{ \Infer{(RW)}{A \lra A, B}{\Infer{(Ax)}{A \lra A}{}} \AND \Infer{(RW)}{B \lra A, B}{\Infer{(Ax)}{B \lra B}{}} } } \]

3.5.1 練習問題

  1. LKにおいて 「 \(A,B,\G \lra \D\) が証明可能 \(\Llra\) \(A \land B,\G \lra \D\) が証明可能」を示せ.

3.6 推論体系LKX

LKと良く似た推論体系LKXの推論規則を以下に示す (LKXはこのテキスト中で用いる名称).

\(\Infer{(Ax)}{\G_1,A,\G_2 \lra \D_1,A,\D_2}{}\)  
\(\Infer{(L\F)}{\G_1,\F,\G_2 \lra \D}{}\)
\(\Infer{(R\F)}{\G \lra \D_1,\F,\D_2}{\G \lra \D_1,\D_2}\)
\(\Infer{(L\T)}{\G_1,\T,\G_2 \lra \D}{\G_1,\G_2 \lra \D}\)
\(\Infer{(R\T)}{\G \lra \D_1,\T,\D_2}{}\)
\(\Infer{(L\land)}{\G_1,A\land B,\G_2 \lra \D}{\G_1,A,B,\G_2 \lra \D}\)
\(\Infer{(R\land)}{\G \lra \D_1,A\land B,\D_2}{\G \lra \D_1,A,\D_2 \AND \G \lra \D_1,B,\D_2}\)
\(\Infer{(L\lor)}{\G_1,A\lor B,\G_2 \lra \D}{\G_1,A,\G_2 \lra \D \AND \G_1,B,\G_2 \lra \D}\)
\(\Infer{(R\lor)}{\G \lra \D_1,A\lor B,\D_2}{\G \lra \D_1,A,B,\D_2}\)
\(\Infer{(L\imp)}{\G_1,A\imp B,\G_2 \lra \D_1,\D_2}{\G_1,\G_2 \lra \D_1,A,\D_2 \AND \G_1,B,\G_2 \lra \D_1,\D_2}\)
\(\Infer{(R\imp)}{\G_1,\G_2 \lra \D_1,A\imp B,\D_2}{\G_1,A,\G_2 \lra \D_1,B,\D_2}\)
\(\Infer{(L\lnot)}{\G_1,\lnot A,\G_2 \lra \D_1,\D_2}{\G_1,\G_2 \lra \D_1,A,\D_2}\)
\(\Infer{(R\lnot)}{\G_1,\G_2 \lra \D_1,\lnot A,\D_2}{\G_1,A,\G_2 \lra \D_1,\D_2}\)
  • LKXにはWeakening, Contraction, Exchangeなどの構造規則が存在しない.
  • LKXにはカット規則も存在しない.

3.6.1 証明図の例

以下はLKXでの \(\lra A \lor \neg A\) の証明図である. \[ \Infer{(R\lor)}{\lra A \lor \neg A}{ \Infer{(R\neg)}{\lra A, \neg A}{ \Infer{(Ax)}{A \lra A}{} }} \]

3.6.2 練習問題

  1. LKXでの \(\neg(A \land \neg B) \lra A \imp B\) の証明図を求めよ.
  2. LKXでの \(A \imp B \lra \neg(A \land \neg B)\) の証明図を求めよ.
  3. LKXでの \(A \imp (B \imp C) \lra (A \imp B) \imp (A \imp C)\) の証明図を求めよ.

3.6.3 seqprover

seprover (http://bach.istc.kobe-u.ac.jp/seqprover/) は, LKXと同様の体系で,与えられたシーケントの証明図を探索するプログラムである. プログラムはPrologで記述されており,約1000行である.

Trying to prove with threshold = 0

----------- Ax  ----------- Ax   ----------- Ax  ----------- Ax
p,q --> p,q     p,r --> p,q      p,q --> p,r     p,r --> p,r
--------------------------- L\/  --------------------------- L\/
      p,q\/r --> p,q                   p,q\/r --> p,r
      --------------- R\/              --------------- R\/
      p,q\/r --> p\/q                  p,q\/r --> p\/r
      ------------------------------------------------ R/\
                  p,q\/r --> (p\/q)/\p\/r
                  ------------------------ L/\
                  p/\q\/r --> (p\/q)/\p\/r

# Proved in 10 msec.

3.6.4 練習問題

  1. seqproverを用いて \(\neg(p \land \neg q) \lra p \imp q\) の証明図を求めよ.
  2. seqproverを用いて \(p \imp q \lra \neg(p \land \neg q)\) の証明図を求めよ.
  3. seqproverを用いて \(p \imp (q \imp r) \lra (p \imp q) \imp (p \imp r)\) の証明図を求めよ.

3.6.5 LKとLKXの比較

  • 証明図を書くのは,LKXのほうがずいぶん簡単だ. 下から上に証明図を書く時,どの規則を適用しても良いし, カット規則もない.
  • では,LKXで証明できたシーケントは, LKでも証明できるのだろうか? また,その逆はどうなのだろうか? すなわち,以下が成り立つだろうか?

    \(\G \lra \D\) がLKで証明可能 \(\Llra\) \(\G \lra \D\) がLKXで証明可能

  • 上記の証明は後回しにして,形式的体系の同等性について考える.

3.6.6 形式体系の同等性

LKの \({\rm L\land_1}\), \({\rm L\land_2}\), \({\rm R\lor_1}\), \({\rm R\lor_2}\), \({\rm L\imp}\) の推論規則を削除して,以下の推論規則を追加した体系をLK'とする.

\(\Infer{(L\land)}{A\land B,\G \lra \D}{A,B,\G \lra \D}\)  
\(\Infer{(R\lor)}{\G \lra \D,A\lor B}{\G \lra \D,A,B}\)
\(\Infer{(L\imp)}{A\imp B,\G \lra \D}{\G \lra \D,A \AND B,\G \lra \D}\)

この時,以下が成り立つ.すなわちLKとLK'は同等である.

LKで \(\G \lra \D\) が証明可能 \(\Llra\) LK'で \(\G \lra \D\) が証明可能

証明
(\(\Lra\))

LKの証明図の高さに関する帰納法で証明する.

LKの証明図の高さが1の場合. 証明図は始シーケントのみから成るが,そのままでLK'の証明図である.

高さが \(h\) 以下のLKの証明図について定理が成り立つと仮定し, 高さが \(h+1\) のLKの証明図について, LK'の証明図が構成できることを示す.

最後の推論規則が \({\rm L\land_1}\), \({\rm L\land_2}\), \({\rm R\lor_1}\), \({\rm R\lor_2}\), \({\rm L\imp}\) 以外の場合,明らかにLK'での証明図を構成できる.

LKの証明図の最後の推論規則が \({\rm L\land_1}\) とする. \[ \Infer{(L\land_1)}{A\land B,\G \lra \D}{A,\G \lra \D} \] この時,以下のようにしてLK'での証明図を構成できる. \[ \Infer{(Cut)}{A\land B,\G \lra \D}{ \Infer{(L\land)}{A\land B \lra A}{ \Infer{(LW)}{A,B \lra A}{ \Infer{(Ax)}{A \lra A}{} }} \AND A,\G \lra \D } \] LKの証明図の最後の推論規則が \({\rm L\imp}\) とする. \[ \Infer{(L\imp)}{A\imp B,\G,\Pi \lra \D,\Sigma}{ \G \lra \D,A \AND B,\Pi \lra \Sigma} \] この時,以下のようにしてLK'での証明図を構成できる. ただし (*W) は複数のWeakening規則の適用を表す. \[ \Infer{(L\imp)}{A\imp B,\G,\Pi \lra \D,\Sigma}{ \Infer{(*W)}{\G,\Pi \lra \D,\Sigma,A}{\G \lra \D,A} \AND \Infer{(*W)}{B,\G,\Pi \lra \D,\Sigma}{B,\Pi \lra \Sigma} } \] LKの証明図の最後の推論規則が他の規則の場合も同様に示される.

(\(\Lla\))

省略.

3.6.7 練習問題

  1. 上の証明を完成させよ.

3.6.8 LKXで証明可能ならばLKで証明可能

LKXで \(\G \lra \D\) が証明可能 \(\Lra\) LKで \(\G \lra \D\) がカット規則を用いずに証明可能

3.6.8.1 TODO 証明

上に示されているようにLKXで証明可能なシーケントは LKでも証明可能である.

では,逆は成立するのだろうか? LKにはカット規則があるが,LKXにはカット規則がないため, 簡単には示せないように思えるが,実際には成立する. このことは,以下の健全性と完全性の節で示す.

3.6.9 練習問題

  1. 上の証明を完成させよ.

3.7 健全性と完全性

以下ではLKの 健全性 (soundness) と 完全性 (completeness) について述べる.

images/sound-and-complete.png

3.7.1 健全性

  • LKで証明可能なシーケントはすべて正しいのだろうか? 間違ったシーケントが証明されることはないのだろうか?
  • 以下に示すように,LKで導出できる(証明可能な)シーケントは すべて「恒真」である.
  • その意味で,LKは 健全 (sound)である.

3.7.2 シーケントの恒真性の定義

シーケントの恒真性を定義するために,以下の記法を導入する. \begin{eqnarray*} (A_1,A_2,\ldots,A_n)_* & = & \neg A_1 \lor \neg A_2 \lor \cdots \lor \neg A_n \\ (B_1,B_2,\ldots,B_n)^* & = & B_1 \lor B_2 \lor \cdots \lor B_n \end{eqnarray*} ただし \(n=0\) の時 \((A_1,A_2,\ldots,A_n)_* = \F\), \((B_1,B_2,\ldots,B_n)^* = \F\) とする.

シーケント \(\G \lra \D\) が恒真とは, \(\G_* \lor \D^*\) が恒真のことと定義する.

3.7.3 LKの健全性

LKで \(\G \lra \D\) が証明可能 \(\Lra\) \(\G_* \lor \D^*\) が恒真

証明

LKの各規則について,上の全シーケントが恒真の時, 下のシーケントが恒真になることを示せば良い.

たとえば \((L\imp)\) について, \(\G_* \lor \D^* \lor A\) および \(\neg B \lor \Pi_* \lor \Sigma^*\) が恒真とする. この時,以下より \(\neg (A \imp B) \lor \G_* \lor \Pi_* \lor \D^* \lor \Sigma^*\) は恒真である. \begin{eqnarray*} & & \neg (A \imp B) \lor \G_* \lor \Pi_* \lor \D^* \lor \Sigma^* \\ & \Equ & (A \land \neg B) \lor (\G_* \lor \Pi_* \lor \D^* \lor \Sigma^*) \\ & \Equ & (A \lor \G_* \lor \Pi_* \lor \D^* \lor \Sigma^*) \land (\neg B \lor \G_* \lor \Pi_* \lor \D^* \lor \Sigma^*) \end{eqnarray*} 他の規則についても同様に示される.

3.7.4 練習問題

  1. 上の証明を完成させよ.

3.7.5 完全性

  • 逆に,恒真なシーケントはすべてLKで証明可能だろうか?
  • 以下に示すように, すべての恒真なシーケントはLKで証明可能である.
  • その意味で,LKは 完全 (complete)である.

3.7.6 LKXの完全性

まず,LKではなくLKXの完全性を示す. そのため,以下の補題を証明する.

  1. LKXの始シーケントは恒真である.
  2. LKXの下シーケントが恒真ならば, 上シーケントはすべて恒真である.
証明

省略.

任意のシーケント \(\G \lra \D\) について以下が成り立つ.
   \(\G_* \lor \D^*\) が恒真 \(\Lra\) LKXで \(\G \lra \D\) が証明可能

証明

\(\G\) および \(\D\) に現れる論理結合子の合計の個数 \(k\) に関する帰納法で証明する.

\(k=0\) の時 \(\G\) および \(\D\) はすべて命題変数あるいは命題定数である. この時 \(\G_* \lor \D^*\) が恒真となるためには, \(\G\) と \(\D\) に共通の命題変数が含まれているか, \(\G\) に \(\F\) あるいは \(\D\) に \(\T\) が含まれていなければならない. したがって \(\G \lra \D\) はLKXの始シーケントとして証明可能である.

\(k>0\) の時 \(\G \lra \D\) には論理結合子が含まれている. その論理結合子に対応し, \(\G \lra \D\) を下シーケントとするLKXの推論規則を \(r\) とすると, \(r\) は下のどちらかの形である. \begin{eqnarray*} \Infer{(r)}{\G \lra \D}{\G_1 \lra \D_1} & \qquad & \Infer{(r)}{\G \lra \D}{\G_1 \lra \D_1 \AND \G_2 \lra \D_2} \end{eqnarray*} 今,仮定より \(\G_* \lor \D^*\) は恒真であるから, 補題より上シーケントもまた恒真である. したがって,帰納法の仮定より上シーケントはLKXで証明可能であり, 推論規則 \(r\) の適用により \(\G \lra \D\) も証明可能である.

3.7.7 練習問題

  1. 上の補題の証明を完成させよ.

3.7.8 LKの完全性

\(\G_* \lor \D^*\) が恒真 \(\Lra\) LKで \(\G \lra \D\) が証明可能

証明

LKXで証明可能なシーケントは, LKでも証明可能であるので,LKも完全である.

3.8 カット除去定理

LKで \(\G \lra \D\) が証明可能 \(\Lra\) LKで \(\G \lra \D\) がカット規則を用いずに証明可能

証明

LKで証明可能なシーケントは,LKの健全性より,恒真であり, 恒真なシーケントは,LKXの完全性より,LKXで証明可能である. LKXで証明可能なシーケントはLKでカット規則を用いずに証明可能である.

3.8.1 LKの無矛盾性

推論体系において \(A\) と \(\neg A\) の双方が証明可能な時, その推論体系は 矛盾 (inconsistent)すると呼ばれる. そうでない時,その推論体系は 無矛盾 (consistent)であると呼ばれる.

LKで \(\lra A\) と \(\lra \neg A\) の双方が証明可能な時, 以下のように空のシーケントが証明可能になる. \[ \Infer{(Cut)}{\lra}{ \lra \neg A \AND \Infer{(L\neg)}{\neg A \lra}{\lra A} } \] また空のシーケントからは \({\rm LW}\), \({\rm RW}\) 規則により 任意のシーケントが証明可能になってしまう.

LKは無矛盾なのだろうか?

まず,LKのカット除去定理から,LKでは空のシーケントは証明できないことがわかる. カット規則以外の推論規則を良く見ると, 下シーケントが空のシーケントになりえるものは存在しない. したがって,LKで \(\lra A\) と \(\lra \neg A\) の双方が証明可能になることはなく, LKは無矛盾である.

4 融合原理

融合原理 (導出原理; resolution principle)は, 1965年にロビンソン (John Alan Robinson)により導入された体系である.

4.1 節と節集合

命題論理式に対する融合原理では, 命題論理式の連言標準形 (CNF)の集合表現を対象とする. 連言標準形 (CNF)の詳細については 命題論理式の 選言標準形と連言標準形 の節を参照のこと.

  • 命題変数あるいは命題変数の否定を リテラル (literal)という. また,命題変数のリテラルを 正リテラル (positive literal), 命題変数の否定のリテラルを 負リテラル (negative literal)という.
  • 0個以上のリテラルの集合を (clause)という.
  • 0個以上の節の集合を 節集合 (set of clauses)という. 元の論理式と同値な節集合を,元の論理式の 節形式 (clausal form)という.
  • 節 \(\{L_1, L_2, \ldots, L_m\}\) は \(L_1 \lor L_2 \lor \cdots \lor L_m\) を表す. 特に,空の節は \(\F\) を表すことに注意する. 空の節は 空節 (empty clause)と呼ばれ \(\Box\) で表される.
  • 節集合 \(\{C_1, C_2, \ldots, C_n\}\) は \(C_1 \land C_2 \land \cdots \land C_n\) を表す. 特に,空の節集合は \(\T\) を表すことに注意する.
  • 一般に,節 \(\{\neg p_1, \neg p_2, \ldots, \neg p_m, q_1, q_2, \ldots, q_n\}\) は \((p_1 \land p_2 \land \cdots \land p_m) \imp (q_1 \lor q_2 \lor \cdots \lor q_n)\) を表す. 特に \(m=0\) の場合 \(\T \imp (q_1 \lor q_2 \lor \cdots \lor q_n)\) すなわち \(q_1 \lor q_2 \lor \cdots \lor q_n\) を表し, \(n=0\) の場合 \((p_1 \land p_2 \land \cdots \land p_m) \imp \F\) すなわち \(\neg(p_1 \land p_2 \land \cdots \land p_m)\) を表す. \(m=0\) かつ \(n=0\) の場合 \(\T \imp \F\) すなわち \(\F\) を表す.

4.1.1 ホーン節

  • 節のうち,正リテラルの個数が高々一つのものを ホーン節 (Horn clause)という.
  • 特に,ホーン節で正リテラルが一つのものを 確定節 (definite clause), 正リテラルを含まないものを ゴール節 (goal clause)という.
  • すべての命題論理式は論理的に同値なあるいは充足同値な節集合に変換できるが, ホーン節の集合に変換できるわけではない.
  • しかし,一階論理のホーン節ではあるが, 論理型プログラミング言語のPrologがホーン節上の融合原理に基づいているという点で, ホーン節は重要な応用を持っている.

4.2 融合

  • \(C_1 = \{P_1,\ldots,P_m\}\), \(C_2 = \{Q_1,\ldots,Q_n\}\) を節とする.また \(P_1\) が命題変数で \(Q_1\) がその否定となっているとする (すなわち \(\neg P_1 = Q_1\)).
  • このとき節 \(C = \{P_2,\ldots,P_m,Q_2,\ldots,Q_n\}\) を得ることを 融合 (導出; resolution)と呼び \(C\) を 融合節 (導出節; resolvent)と呼ぶ.
  • \(C\) はリテラルの集合であるので, 同一のリテラルは一つにまとめられる点に注意すること. 同一のリテラルをまとめる処理を factoring という.

4.2.1 融合の例

  • \(C_1 = \{\neg p, q\}\), \(C_2 = \{p, r\}\) から 融合により融合節 \(C = \{q, r\}\) が得られる (\(P_1 = \neg p\), \(Q_1 = p\) とする).
  • \(C_1 = \{\neg p, q\}\), \(C_2 = \{p, q, r\}\) から 融合により融合節 \(C = \{q, r\}\) が得られる (\(P_1 = \neg p\), \(Q_1 = p\) とする). factoring 処理が行われている点に注意する.
  • \(C_1 = \{\neg p, \neg q\}\), \(C_2 = \{p, q, r\}\) から 融合により融合節 \(C = \{\neg q, q, r\}\) が得られる (\(P_1 = \neg p\), \(Q_1 = p\) とする). また \(C' = \{\neg p, p, r\}\) も得られる (\(P_1 = \neg q\), \(Q_1 = q\) とする). \(\{r\}\) は融合節ではないことに注意する.

4.2.2 練習問題

  1. 融合節として空節が得られるのはどのような場合か.
  2. \(C_1 = \{\neg p, q\}\), \(C_2 = \{p, r\}\) から 融合節 \(C = \{q, r\}\) を得る推論は, LK で \(\neg p \lor q, p \lor r \lra q \lor r\) を証明することに対応する. このシーケントを LK で証明せよ.

4.3 融合原理と反駁による証明

融合による推論は,すべての恒真なシーケントを導出できるわけではない. たとえば \(p, q \lra p \lor q\) は恒真なシーケントだが, 節 \(\{p,q\}\) は節 \(\{p\}\) と \(\{q\}\) から導出できない.

そこで融合原理では 反駁による証明 (proof by refutation, 背理法による証明)を行う. すなわち仮定 \(A\) の元で結論 \(B\) を導出したい場合, 仮定に結論の否定を付け加えた \(A \land \neg B\) の節形式を考え, その節形式から融合により空節を導く. 空節が導き出されれば, 後で述べるように \(A \land \neg B\) が充足不能であること, すなわち \(A \imp B\) が恒真であることがわかる.

したがって,融合原理における反駁手続きは, 与えられた節集合 \(\G\) から空節 \(\Box\) を導出する手続きである.

融合原理の推論規則は以下のように表すことができる

\(\Infer{}{\G \lra C}{}\)
(provided \(C \in \G\))
\(\Infer{}{\G \lra C}{\G \lra C_1 \AND \G \lra C_2}\)
(provided \(C\) is a resolvent of \(C_1\) and \(C_2\))

4.3.1 融合原理の証明図と反駁木

節集合 \(\G = \{\{\neg p,\neg q\}, \{\neg p,q\}, \{p,\neg q\}, \{p,q\}\}\) から空節を導出する証明図の例を以下に示す \[ \Infer{}{\G \lra \Box}{ \Infer{}{\G \lra \{\neg p\}}{ \Infer{}{\G \lra \{\neg p, \neg q\}}{} \AND \Infer{}{\G \lra \{\neg p, q\}}{} } \AND \Infer{}{\G \lra \{p\}}{ \Infer{}{\G \lra \{p, \neg q\}}{} \AND \Infer{}{\G \lra \{p, q\}}{} } } \] 融合原理による反駁を示すには, 通常は以下のような 反駁木 (refutation tree)が用いられる (導出した節を複数回用いることもあるので,正確には木ではなくDAGである).

images/resolution1_1ca0e62b9e2352370e5aae05a890c25cb4a4130f.png

以下は,同一の節集合に対する別の反駁木である.

images/resolution2_5214b23e1a7fcaaf707cd1bef8f002d4c01a720f.png

4.3.2 練習問題

  1. 節集合 \(\{\{p,q\}, \{\neg p,r\}, \{\neg p,\neg r\}, \{p,\neg q\}\}\) から空節を導出せよ.
    (解答例)

    以下のように導出できる.

    1. \(\{p,q\}\)
    2. \(\{\neg p,r\}\)
    3. \(\{\neg p,\neg r\}\)
    4. \(\{p,\neg q\}\)
    5. \(\{p\}\) (1, 4から)
    6. \(\{r\}\) (2, 5から)
    7. \(\{\neg r\}\) (3, 5から)
    8. \(\Box\) (6, 7から)
  2. 節集合 \(\{\{p,q,\neg r,s\}, \{\neg p,r,s\}, \{\neg q,\neg r\}, \{p,\neg s\}, \{\neg p,\neg r\}, \{r\}\}\) から空節を導出せよ.
  3. 仮定 \((p \imp q) \imp (p \imp r)\) から結論 \(p \imp (q \imp r)\) が導かれることを 反駁により示せ. すなわち \(((p \imp q) \imp (p \imp r)) \land \neg (p \imp (q \imp r))\) の節形式から 空節が導出可能であることを示せ.
  4. コイン投げで「表なら私の勝ち」,「裏ならあなたの負け」とする. この時,常にあなたが負けることを示せ.
    (解答例)

    表を \(h\), 裏を \(t\), 私の勝ちを \(m\), あなたの勝ちを \(y\) で表す. 仮定は節 \(\{h,t\}\), \(\{\neg h,\neg t\}\), \(\{m,y\}\), \(\{\neg m,\neg y\}\), \(\{\neg h,m\}\), \(\{\neg t,\neg y\}\) で表すことができる. 結論の否定は \(\{y\}\) という節になる. これらの節から空節が導出できることを示せば良い.

4.4 融合原理の健全性と完全性

反駁手続きにおいて,融合原理は健全かつ完全である. すなわち節集合 \(\G\) について以下が成り立つ.

\(\G\) から融合により空節が導出可能 \(\Llra\) \(\G\) が充足不能

4.5 融合戦略

融合原理は反駁に対して完全であるが, 融合により導出できる節の組合せが膨大であり, 探索空間が巨大である. そこで,反駁探索のための様々な戦略が提案されている.

4.5.1 単位融合戦略

単位融合 (unit resolution)では, 融合の一方をリテラルが一つだけの単位節に制限する. 単位融合戦略はホーン節に対しては完全だが,一般の節に対しては完全ではない.

4.5.2 入力融合戦略

入力融合 (input resolution)では, 融合の一方を最初に与えられた節集合中の節に制限する. 入力融合戦略はホーン節に対しては完全だが,一般の節に対しては完全ではない.

4.5.3 線形融合戦略

線形融合 (linear resolution)では, 融合の一方を以下のいずれかに制限する.

  1. 最初に与えられた節集合中の節
  2. これまでに得られた融合節

線形融合戦略は,ホーン節だけでなく一般の節に対しても完全である.

4.5.4 SLD融合戦略

SLD融合 (Selective Linear Resolution for Definite Clauses)は, ホーン節に対する融合である.

融合の一方は負リテラルだけからなるゴール節である (充足不能な節集合中にゴール節は必ず存在する). ゴール節から一つのリテラルを任意の方法で選択する. 融合の他方は選択したリテラルの相補リテラルを含む確定節である. すなわち以下のような導出を行う. \[ \Infer{}{\{\neg Q_1,\ldots,\neg Q_n,\neg P_2,\ldots,\neg P_m\}}{ \{P_1,\neg Q_1,\ldots,\neg Q_n\} \AND \{\neg P_1,\neg P_2,\ldots,\neg P_m\} } \] 論理型プログラミング言語Prologにおける計算は,SLD導出が基になっている (ただしPrologでの処理は,単純な深さ優先探索のため完全ではない).

4.5.5 練習問題

  1. 節集合 \(\{\{\neg p,\neg q\}, \{\neg p,q\}, \{p,\neg q\}, \{p,q\}\}\) に対して, 各種の戦略で空節が導出可能かどうかを確かめよ.

Date:

Author: 田村直之

Org version 7.8.02 with Emacs version 24

Validate XHTML 1.0