数理解析研究所講究録 1325 巻 2003 年 233-237

233
類推機能をもった対話型シークェント計算証明システムの開発
山田 敬三, 平田 耕一, 原尾 政輝

九州工業大学 情報工学部〒 820-8502 福岡県 飯塚市 川津 680-4{yamada,hirata,harao}@ai.kyutech.ac.jp

シークェント計算に基づく証明は人間にとって解かりやすく教育支援をはじめ多くの応用が可能である. しかしながら, 推論過程が複雑なため自動化は困難である. 本稿では, 類推機構を導入することによってあらまし:

半自動的に機能する対話型シークェント証明システムの開発をしたので, その概要について述べる.

Developping lntaractive Sequent Caliculus Prover
Based on Analogy
Keizo Yamada,Kouich Hirata,and Masateru Harao

Department of Artificial Intelligence
Kyushu Institute of Tecnology
Kawazu 680-4, Iizuka 820-8502, Japan{yamada,hirata,harao}@ai.kyutech.ac.jp
humm, it hae many applications
abstract: Since aproof based on sequent calculus is easy to understand for
its inference process isincluding computer aided education. However, it is difficult to automate because
by introducing an analogycalcomplex. We develop an interactive semi-automated sequent calculus prover
reasoning mechanism. In this PaPer, we demonstrate the outline of our system.

1

はじめに$\mathrm{L}\mathrm{K}$現在, 自動証明システムの多くは, タブロー法や PrO$\log$に代表される導出原理といった論理体系が用いられている. それらは, 計算機で処理しやすい反面, 証明過程は人間には理解しにくい. \llcorner かしながら, 論理学の教育支援に用いたり, 証明からプログラムを抽出する場
合, あるいは数学の証明システムへの応用などでは, 証明可能か否かを問うだけではなく, その証明過程が重要になる. そこで, 人間が直観的に理解しやすい論理体系を自動化し証明過程の表示機能や操作機能などを計算機上に実現することで, 有用なシステムを構築すことが期待できる. このような観点から, 我々は, 人間が直観的に証明過程を理解することのできる, 古典論理シークエント計算の自動化を行った.
シークエント計算には用いる規則が多数あり, 規の体系である$\mathrm{L}\mathrm{K}$則の適用の仕方が複雑になるため証明の自動化が 困難である. そこで, 本稿ではヒューリステイソクを用$\mathrm{A}\mathrm{a}$た

自動化の方法として, スキーマ誘導による類推 [1] を導入する. スキーマとは一般化された知識であり, 問題のパターンを表し, 類似性の判定に用いる. また, スキーマ誘導方式とは, スキーマと未知の問題との類似性がらその問題の解を導出する仕組みである. この類推の実現にあたっては, 多くのスキーマを蓄え, その中がら適切なスキーマを探し出す必要がある. 本稿で G よそのためのスキーマベースの設計と探索法につし\supset て考察する.
$\mathrm{L}\mathrm{K}$

証明は木構造の図で表されるが, その証明図を計

234算機上で見やすく表示するためには工夫が必要である.
な証明図を表示するシステ として, XIsabelle や$\text{ム}$$\mathrm{x}\mathrm{p}\mathrm{e}$どがあるが, 証明の操作が簡潔でない, 述語論理が扱えないといった難点がある. このような難点を克服した,直観的に見やすく操作性のよいシステムを構築すれば,教育支援などへの応用が期待できる. 本稿では, まず,シークエント計算の証明図を直接表示できるシス
テ A を作り, 類推によって自動的に得られた証明を表示したり, 規則を 1 ステツプごとに簡潔な操作で適用して証明することもできる対話的証明機能を実現する.
本稿の構成は以下の通りである. まず, 2 節で, 本研
シークエント計算について述べ, 3 節で究で用いる類推処理について述べる. 4 節では, 類推処理のため$\mathrm{L}\mathrm{K}$$(\forall(\forall p・x・\forall x(z_{\forall}p.・p’.(x)(xxp・p.(x))\Lambda(\forall x.q(x))\vdash p(z)\Lambda q(z)x))\Lambda(\forall x.q(x))\supset\forall x.(p(_{X})\Lambda q(x))^{\supset-}))\Lambda(\forall x.q(x))\vdash\forall x.(p(x)\Lambda q(x))^{\forall-\text{右}}(z),\forall x.q(x)\vdash p(z)\Lambda q(_{Z})^{\forall-\text{左_{}\Lambda-\text{左}^{}\wedge-:B}}q(z_{Z})\vdash p(z)p(z),q(z)\vdash q(z)p(x),\forall x.q(x)\vdash p(z)\Lambda q(z)^{\forall-\mathit{2}\in}p(),q(z)\vdash p(z)\Lambda q(z)$–右–$\vdash$

図 1:$(\forall x.p(x))\Lambda(\forall x.q(x))\supset\forall x.(p(x)\Lambda q(x))$の証

明図$\mathrm{L}\mathrm{K}$$\frac{\Gamma\vdash\Delta,A}{\neg A,\Gamma\vdash\Delta}$のスキーマベースの設計, および探索法について議論

(,-左)

.

する. 最後に, 5 節でシステムの実装の概要について述$\frac{\forall x.A,A[x.--t],\Gamma\vdash\Delta}{\forall x.A,\Gamma\vdash\Delta}$

べる.

(\neg 一右)$\frac{A,\Gamma\vdash\Delta}{\Gamma\vdash\Delta,\neg A}$.

(\forall -左)(\forall 一右)$\frac{\Gamma\vdash\Delta,\forall x.A,A[x\cdot=z]}{\Gamma\vdash\Delta,\forall x.A}$

2

.

準備

$\frac{\exists x.A,A[x.--z],\Gamma\vdash\Delta}{\exists x.A,\Gamma\vdash\Delta}$$A_{1},$$A_{m},B_{1},$$\cdots,$$\cdots,$$B_{n}$をそれぞれ論理式とする. こ.のとき, 以下の 0 個以上の述語論理式の列の組をシークエント (sequent) と う.

$\frac{\Gamma\vdash\Delta,\exists x.A,A[x.=t]}{\Gamma\vdash\Delta,\exists x.A}$(\exists -左)(\exists 一右)$\mathrm{A}^{\mathrm{a}}$ただし, 図中 $A[x:=s]$ は $A$ における変数 の自由な出現を項 で置き換えた式を表す. また, は任意の項$x$$A_{1},$$\cdots,$$A_{m}\vdash B_{1},$ $\cdots,$ $B_{n}$

$t$

$s$

シークエントは, 直観的には$A_{1},$$\cdots,$$A_{m}$

を仮定するとのいずれかが成り立つことを表している.の左右に同じ論理式が現れるシークエント
さらに,をそれぞれシークエを公理 (oxiom) という.

$B_{1},$$\cdots,$$B_{n}$

は変数条件を満たす変数とする. すなわち,は下式に自由には現れない変数とする.とし,$\vdash$$S_{1},$$S_{2},$$S$ントとする. このとき, 推論規貝り$(infer\mathrm{r}_{d}nce\tau^{u}ule)$とは,次の形をした図である:$\frac{s_{1}}{s}$または推論規則は, 直観的にはしいことを表している.

$\frac{S_{1}S_{2}}{s}$$S_{1}(S_{2})$

$z$

$z$

証明図とは、最も下の式から出発して順次推論規則を適用して得られる図であり, シークエントを節とすからる木構造になっている. 論理式 $P$ に対して,$P$その葉がすべて公始まる証明図を の証明図といい,$\vdash P$理となるとき, $P$ は証明可能という. 例えば, 論理式.

が正しいとき, $S$ は正シークエント計算の推論規則にはいくつかの体系がある [3] が, 本稿では, 以下の$(\forall x.p(x))\Lambda(\forall x.q(x))\supset\forall x.(p(x)\Lambda q(x))$の証明図は図1 のようになる.

$\mathrm{L}\mathrm{K}$12 種類を用いる:

3$\frac{B,\Gamma\vdash\Delta\Gamma\vdash A,\Delta}{A\supset B,\Gamma\vdash\Delta}$(っ左)

スキーマ誘導による類推
本システ$\text{ム}$では, スキーマ誘導型の類推 [1] を用いて証明を半自動化する.

スキーマとは論理式のパターンであり, 型付き二階$\frac{A,\Gamma\vdash\Delta,B}{\Gamma\vdash\Delta,A\supset B}(\supset-\ddagger \mathrm{j})$項で定義される [4], 論理式に述語変数を許す表現であ$\frac{A,B,\Gamma\vdash\Delta}{A\wedge B,\Gamma\vdash\Delta}$(\triangle 一左)$\frac{\Gamma\vdash\Delta,A\Gamma\vdash\Delta,B}{\Gamma\vdash\Delta,A\Lambda B}$$\frac{A,\Gamma\vdash\Delta\Gamma\vdash\Delta,B}{A\vee B\Gamma\vdash\Delta}$$\frac{\Gamma\vdash\Delta,A,B}{\Gamma\vdash\Delta,A\vee B}$(V 一右)

証明スキーマとはスキーマの証明である. スキーマとその証明スキーマの組を蓄積したものをスキーマる.

(\Lambda -右)

ベースという.

(\vee 一左)類推とは 「似た問題は似た解法をもつ」 という原理に基づく推論であり, 一般には正しいとは限らない. 類
推証明においては, 推論の正しさを保存するような類似235 235,$\Phi_{1}=P\supset P$,$\Phi_{2}=(P\vee(Q\Lambda\neg Q))\supset P$$\Phi_{3}=P\supset(\neg P\supset(P\Lambda\neg P))$$\Phi_{4}=P\supset(Q\supset P)$,$\Phi_{5}=P\supset(Q\supset(P\Lambda Q))$$\Phi_{6}=P\supset(\neg P\supset Q)$$\Phi_{7}=(P\Lambda Q)\supset P$

図 2: スキーマ誘導型類推の概要,,,$\Phi_{8}=(P\Lambda(P\supset Q))\supset Q$,$\Phi_{9}=(\neg P\vee Q)\supset(P\supset Q)$性の定義が重要になる. そのため, 本システムでは, 類似性の判定にスキーママツチング [2] を用いる. スキーママッチングは, 論理的な正しさを保つ代入のみを導出するので, 提案するスキーマ誘導類推により常に正しい証明を得ることができる. 本システムにおける未知の問題 の類推による証明は以下の手順による:
まず, 証明の指針となるいくつかの誘導問題とその証明を抽象化し, スキーマベースに蓄える.

,,,$\Phi_{10}=(P\supset R)\supset((Q\supset R)\supset((P\vee Q)\supset R))$$\Phi_{11}=\exists x.P(x)\vee\exists x.Q(x)\supset\exists x.(P(x)\vee Q(x))$$\Phi_{12}=\forall x(P(x)\supset Q(x))\Lambda\exists x.P(x)\supset\exists x.Q(x)$$\Phi_{13}=\exists x.(P(x)\Lambda Q(x))\Lambda\forall x(P(x)\supset h(x))$$\Lambda(\forall xQ(x)\supset r(x))\supset\exists x.(h(x))\Lambda r(x))$$\Phi_{14}=\forall x(P(x)\supset Q(x))\Lambda P(c)\supset\exists x.Q(x)$$\varphi$

1. 未知の問題$\varphi$とマッチする誘導問題のスキーマ,,,.

図 3: スキーマベース $SB$ に含まれるスキーマ$\Phi$を探索する.

2. 探索に成功したとき,となる を計算する.
(a)の証明を導出する.
により(b) Pr。
$\theta$$\Phi\theta=\varphi$$\theta$$\varphi$

3. 探索に失敗したとき,

01: function search $(\varphi, SB, C)$ ;
do
while
02:
大きさが最大となる $C\in C$ を適当に選ぶ;
03:$C:=C-\{C\}$ ;04:
がマツチング可能 thenとif
05:
while 各 $(\Phi, P7^{\cdot}\Phi)\in SBc$ に対して do
06:
if と がマツチング可能 then07:とそのときのマツチング代人 を08:$\mathrm{C}\neq\emptyset$(a) 手動で証明する.
(b) その結果をスキーマベースに格納する.

$C$

4

スキーマベース$\varphi$$\Phi$$\varphi$

類推処理においてはマツチするスキーマを効率的に見つけることが重要となる. そのため, スキーマベースをスキーマの特徴に従って階層化し, 探索の効率化技法について述べる.
定義 1 スキーマ$\Phi$の特徴 (proffle)c。とは,$\Phi$に出現するアトムをすべて新しい 0 引数の述詔変数で置き換えた式である. 特徴 C。に現れる論理結合子の数を C ウの大きさといい,$|C_{\Phi}|$で表す.

直観的には, 特徴はスキーマの論理結合子に着目し,その配置を表す.
例えば, スキーマ $\Phi_{1}=\forall x.P(x)\supset\exists x.P(x),$$P\supset Q,$ $\Phi_{3}=P(a, b)$ の特徴はそれぞれ$\Phi_{2}=$$C_{\Phi_{1}}=$$\forall x.P_{1}\supset\exists x.P_{2},$$C_{\Phi_{2}}=\neg P_{3}\supset P_{4},$り, その大きさは.

$C_{\Phi_{3}}=P_{5}$とな$|C_{\Phi_{1}}|=3,$ $|C_{\Phi_{2}}|=1,$ $|C_{\Phi_{3}}|=0$と$\theta$$Pr_{\Phi}$

返して探索を終了する;

09:
10:

end of while($\varphi$

は $c$. とはマツチするが, $SBc$. 中のスキーマとはマツチしない)

11:$C:=\{C’\in C|C\leq C’\}$end of if
13:and of while

12:

探索に失敗して終了する
14:
15: end of function
図 4: スキーマベース探索アルゴリズム

236
なる. 以降では, 特に混乱のない限り$\Phi$の特徴を単に特徴という. また, ここで導入した述語変数の出現は高々1 回となり, 数も持たないので, 以降は特徴に現れる
述語変数はすべて と表し, 束縛変数名も省略する. す,は, それぞれると, 例えば,$\mathrm{e}|$$*$$C_{\Phi_{1}},$$\neg*\supset*,$$*$$C_{\Phi_{2}},$$\forall*\supset\exists*$$C_{\Phi_{3}}$と表わされる.

定義 2 特徴上の二項関係$\leq$と, 特徴 $C$ に対するスキーマベース $SB$ の部分集合 SB。をそれぞれ次のように定義する:
く$=${ $(C,$ $D)|$ ある代入\mbox{\boldmath $\theta$}に対して,$SB_{C}$$=$$\{(\Phi, Pr_{\Phi})\in SB|\Phi\leq C\}$

$C=D\theta$},

図 5: 階層化されたスキーマベース. ただし,は次の通り. $C_{1}=*\supset*,$ $C_{2}=(*\vee*)\supset*,$ $C_{3}=*\supset$.のうち, 同じ特徴を持ったものの集合である.
$\leq$$C_{5}=(**)\supset\exists*,$$C_{6}=$$C_{7}=(*\supset*)\supset(*\supset*),$$c_{8}=$$C_{4}=(*\Lambda*)\supset*,$$(*\supset*),$

直観的には, SB。は $SB$ に蓄えられているスキーマ

命題 1 二項関係$c_{1},$ $\cdots c_{8}$$(*\vee*)\supset(*\supset*),$$(*\Lambda*)\supset\exists*$に対して, 以下の 2 つの性質が成り立つ :1. くは半順序となる.
を特徴とする.
2. $BS$ をスキーマベースとし,$SBc_{1}\subset
SBc_{2}$ が成りならば,このとき,$C_{1},$$C_{2}$$C_{1}\leq C_{2}$

図 6: 本システ

立つ.

本システ A では, 大きさ 3 までの適当な特徴を用いてスキーマベースを階層化する. そして, 論理式 が与え2.

を用いて階層化したスキーマ
ベース $SB$ 内を図 4 に示す探索アルゴリズム Search(\mbox{\boldmath $\varphi$},$SB,$ $C)$が見つかるので,$\Phi_{12},$の概要$\Phi_{13},$$\Phi_{14}\in SB_{C_{8}}$が$\varphi$とマッチング可能か否かを確める.
3. マッチングに失敗するので, $C_{8}\leq C’$ となる $C’$ のうち, もっとも大きなもは C。なので, $SBc_{4}$ につ$\varphi$られたとき, 特徴の集合$C_{8}$$\text{ム}$$C$に従って探索する.

いて$\varphi$とのマツチング可能か否かを調べる.

4. 利用可能なスキーマとして

命題 2 スキーマベースを $SB$ とし, を論理式とする.
このとき, Search が とマツチング可能なスキーマの$\varphi$$\Phi_{7}\in C_{2}$が見つかる.

$\varphi$

探索に失敗するとき, $SB$ 内にそのようなスキーマは存在しない.
$\text{ム}$例 1 図 4 の 14 のスキーマを含むスキーマベース $SB$を以下の 8 の特徴を用いて図 4 のように階層化する:.

$C=\{\begin{array}{llll}c_{1}=*\supset* c_{2}=(**)\supset * C_{3}=*\supset(*\supset*) c_{4}=(*\wedge*)\supset *c_{6}=(**)\supset\exists* c_{6}=(*\vee*)\supset(*\supset*) c_{7}=(*\supset*)\supset(*\supset*) c_{8}=(*\wedge*)\supset\exists* \end{array}\}$次に, 論理式 $\varphi=(\exists x.p(x)\Lambda q)\supset\exists x.p(x)$ が与えられたときの $SB$ の探索過程を示す :1. まず, 図 4 中の特徴のうち, 最も大きい (最下段) も$\varphi$とマツチングするものを探す.

実装
最後に本節では実装したシステムの使い方について

この性質はアルゴリズ の完全性を表している.のの中から5述べる. 本システムでは, 類推による証明と 1 ステツプごとに対話的に証明を進める対話型証明の 2 種類の方法が用意されている. まず, ユーザはシステ\Delta のテキス
トフィールドに証明したい論理式を入力する. ここで,“search” ポタンを押すと, システムはスキーマベースを探索し有効なスキーマをが見つかれば, それを援用して与えられた論理式の証明を返し, 見つからなければ, エラー処理をする.
論理式入力後, “start” ボタンを押すと, システムはその論理式のシークエントを表示して, 対話的証明を開始する. シークエント中の論理式は, すべてボタンで表されており, ユーザはそのポタンを押すことで, システムに, 推論規則を適用するシークエントと論理式を示す. システムは, その指示に従って適切な推論規則を

237
証明を導出する. 2. 利用可能なスキーマがあれば必ず探索は成功するという意味で完全である.
今後の課題として, 証明過程を再利用できるシステの設計・構築が上げられる. そのためには以下の機能が必要となる:
1. その証明の自動的な抽象化.
2. スキーマベースの構成の自動化
また, 十分な証明を行うのに, 必要なスキーマを調べる$\text{ム}$

図 7: 論理式の入力 (左). スキーマベース内で見つかるのも今後の課題である.

有効なスキーマ (右).

参考文献
[1] Harao, M.: Proof discovery in $LK$ system by anal$ogy$ , LNCS 1345, pP.197-211, 1997.

図 8: スキーマを援用して得られた証明 (左). スキーマ

[2] Kubo, K., Yamada, Y., Hirata K. and Harao, M.:
Efficient scherna matching algorithrn based on prechecking , IEICE, J85-D-I, No 2, pp.143-151, 2002.

ベース内で見つかる有効なスキーマ (右)[3] Troelstra, A. S. and Schwichtenberg, H.: Basec
Proof Theory, Cambridge University Press, 1996.

シークエントに適用し, その結果を表示する. ただし,[4] Yamada, Y., Hirata K. and Harao, M.: Schema
matching and its complexity, IEICE, J82-D-I, No

公理に対してさらに推論規則を適用することはできないようになっている.

また, 証明図中の公理に含まれていない論理式ならば, どれでもユーザは選択し, 推論規則を適用すること
このため, 間違えたときの証明のやり直しや, 別解を探すなど, 試行錯誤がしやすくなっている.

ができる.

この特徴は, 類推を用いて得られた証明に対しても同様である. システムの構成は図 5 のようになっている.
例えば, 論理式 $(p\Lambda q)\supset(r\supset(p\Lambda q))$ を類推を用いて証明する場合, 図 5 左のように入力し, “search” ポタンを押す. すると, システ A は適当なスキーマ (図 5右) を見つけ, それを基に証明を出力する (図 5 左). また, 論理式を入力した時点で, “start” ボタンを押せば,
図 5 右のように, 対話的に証明を進めるための準備がなされる.

6考察

本稿では, 類推機能を持ったシークエント計算証明システ\Delta の概要について述べた. 特に, システムを構築する上での要所のひとつであるスキーマベースについて,その構成法と探索法を示た. スキーマの大きな特徴を捉えながら, 効率よく探索するアルゴリズ Search を定式化した. なお, Search には次の性質がある:$\text{ム}$1. 探索アルゴリズムが, 出力したスキーマは正しい

11, pP.1307-1316,1999.