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

\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*}

シーケント \(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\) が推論できない体系は 無矛盾 であるという．

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

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

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

• 後述の論理結合子に関する推論規則とは異なり， シーケントの構造を変更する規則のため構造規則と呼ばれる．
• \(\G\), \(\Pi\), \(\D\), \(\Sigma\) は0個以上の任意の命題論理式の列であり， \(A\), \(B\) は任意の命題論理式である．
• それぞれの規則の名称の意味は以下の通りである．

  名称	意味	日本語の名称
  LW	Left Weakening	増左
  RW	Right Weakening	増右
  LC	Left Contraction	減左
  RC	Right Contraction	減右
  LX	Left Exchange	換左
  RX	Right Exchange	換右

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

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

以下は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}{} }}}}} \]

以下は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}{} }} }}} \]

以下は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}{} }} }}} \]

以下は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}{} }} \]

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.

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

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

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

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

この時，以下が成り立つ．すなわち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\))

省略．

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

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

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

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

シーケントの恒真性を定義するために，以下の記法を導入する． \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^*\) が恒真のことと定義する．

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*} 他の規則についても同様に示される．

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

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

まず，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\) も証明可能である．

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

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

証明

LKXで証明可能なシーケントは， LKでも証明可能であるので，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は無矛盾である．

• 節のうち，正リテラルの個数が高々一つのものを ホーン節 (Horn clause)という．
• 特に，ホーン節で正リテラルが一つのものを 確定節 (definite clause)， 正リテラルを含まないものを ゴール節 (goal clause)という．

• すべての命題論理式は論理的に同値なあるいは充足同値な節集合に変換できるが， ホーン節の集合に変換できるわけではない．
• しかし，一階論理のホーン節ではあるが， 論理型プログラミング言語のPrologがホーン節上の融合原理に基づいているという点で， ホーン節は重要な応用を持っている．

• \(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\}\) は融合節ではないことに注意する．

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 で証明せよ．

節集合 \(\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である)．

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

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

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

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

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

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

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での処理は，単純な深さ優先探索のため完全ではない)．

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