数理解析研究所講究録906 巻 1995 年 138-145

138

自然推論による微積の初歩の完全な形式化とそのプルーフ. チェッカー
Complete Formalization of Some Elementary Calculus Theorems
by Natural Deduction and its Proof-Checker
日大理工数高橋英之 (Hideyuki Takahashi)

日大理工数山下正人 (Masato Yamashita)(現. サンピックシステム(株))

Genzen の自然推論 (を用いた証明) に対する原初的な証明チェッカ要約$\mathrm{P}\mathrm{r}\mathrm{f}\mathrm{C}\mathrm{h}\mathrm{e}\mathrm{C}\mathrm{k}\mathrm{e}\mathrm{r}$を、Prolog で自作した $-$ これはよくある話で、 特に難しい箇所はない。 ついで、 微積の初めによく出てくる極限に関する二、 三のごく簡単な定理を例として、 形式的な証明を考えた。

それらに特殊な問題を扱えるように証明チェッカの拡張を行ないながら、 それらの完全に形式的な証明を作成し、 その証明を証明チェッカにかけて、 通るのを確認した。 この形式

化の方は文献がないわけではないのだが、 多様な定式化を許すであろうこの研究分野にしては研究が少なすぎる。 また普通の数学科の教員・学生にとって familiar なものになっていない。 そこには、 数列をどうコンピュータに教えるか (「無限に対する有限的取り扱い」

問題の

–

部)

だとか、 ‘関数の性質”についての 「日常言語による自然な理解」 をどう形式化するか、 といった困難で興味深い問題がある。 それについてささやかな経験を述べる。

これに関連して次の提言をしたい。 いわゆる 「研究」 とは別に、 学生の論理的な数学学

習を助けることを目的とした 「教育用研究」 があるべきではないか。 そこでは $-$ 方では論
理処理ソフト ($\mathrm{L}\mathrm{o}\mathrm{g}\mathrm{i}\mathrm{c}$a とでも呼ぶべき、 Uathemat ica の論理処理版ソフト)

その他のソフトウェア的環境の整備は勿論であるが、 他方ではそれ以上に、 微積分ほかの数学の、
より

–

\S I

層の形式化、 記号論理化が課題となる。 ここには為すべき多くの仕事がある。

はじめに

孔子研究との関係-

マは$\text{「}$

本研究のモティベーションを述べる。 筆者の $-$ 人 (高橋) の研究テ『論語』 の公理化から孔子の AI 化へ」 というものである [1] 。その方針は次のように二つの領域を結合することである :］生譴髻 価値論の論理体系として公理化する。

孔子は価値論の論理学者 (– 種の数学者) であると見なす。

△修譴 Artificial lathema

139

tician あるいはAutomated Reasoning (自動証明) の研究、 という流れにのせる。 すると

そこにソフトウェアとしての孔子ができるだろう。 / 本講演は

△亡愀犬靴討い襦「ソフトウェアによる孔子 (あるいは数学者) をつくる」 というテーマをトーンダウン
すると、 「コンピュータの中にモラルを学ぶ子ども (あるいは数学を学ぶ学生) をつくる」というテーマ、 さらに 「コンピュータ.

$=|^{}$

モラル(あるいは数学) を教える」 というテーマになる。 そのためにはコンピュータは如何なる装備を有するべきか。

コンピュータに数学を教える ?

．皀薀襪任眇

悗任

見する 「定理発見のメカニズム」 は難しいようだ。

メカニズム」 は、 まだ未知の要素ばかりである。

“

￢紳蠅

３阿

意味のある” 新しい命題を発“意味を理解’ する 「理解のらの命題の、証明を自ら見出だす「証明発見のメカニズム」 は、 低レベルのものなら既に作られている。

ず埜紊法 外から命題とその証明を与えられて、 その証明の正しさを調べる 「証明チェックのメカニズム」
は、 最も単純なものである。 論理なるものの性質上からいっても、 チェックは万人にとって、 特に計算機にもできるものであるはずだ。 / コンピュータが論理を扱うには、 最低限、論理のチェック機構 (証明チェッカ) を持つべきだ。
「チャート式」 はエキスパート. システム ?

こうしたテーマで我々がまず思ったことは、 受験数学の 「チャート式」 なるものは、 ソフト化すれば受験数学のエキスパート. シ

ステムになるのではないかということであった。 エキスパート. システムとは現在成功している人工知能システムで、 こういう状況ではこうしたらよい、 という規則の集積として表される。 だが、 大学の数学については 「チャート式」 の参考書はないようである。

微積形式化の文献は少ない

われわれは当初、 微積分学には完全に記号論理化した理論があるはずだと考えていたが、 実際には数少ない。 文献 [2] は、 自然数から始めて自然数の分数として有理数を定義しデデキントの切断により実数を導入する、 という通例の各段階を形式的論理体系で追って行く。 だが残念なことにすべての証明は概略のみで、 加えて、実数を扱う論理体系が有理数の集合をベースにしており、 不便さ.

見にくさがある。

最近では自動証明や証明チェッカの研究のなかで、 数学の形式的証明の試みもいろいろなされている [3] 。アメ リカには、 全数学の形式的証明をめざそうという呼びかけ$(\mathrm{Q}\mathrm{E}\mathrm{D}$Project) もある。 微積分学の形式化という研究分野はその重要性からして、 たとえ多少の研究が既にあるとしても、 もっと多くの試みがなされるべき分野であると考える。

\S I数列の極限についての簡単な定理

140(1) 証明すべき命題の定式化

まず例題として考えたのは数列の極限に関するごく簡単
有限 (の数学の問題) を有限 (であるコンピュータ) で扱な定理である。 なぜ数列か ?

うのは興味が少ない。 無限 (に関する数学の問題) を有限 (であるコンピュータ) で扱うことが面白い。 数列はその点、 無限性が生まに出てくる問題である。 / 例題として次の命題を証明したい。 証明すべき命題 :1$\mathrm{i}\mathrm{m}\mathrm{n}arrow\infty$

1a$\mathrm{i}\mathrm{m}\mathrm{n}arrow\infty$

1

且つ$\mathrm{n}=\mathrm{P}$( a$\mathrm{n}+\mathrm{b}\mathrm{n}$

)

である。

$=\mathrm{P}+\mathrm{q}$

この命題を、 われわれが定めた簡単な証明記述言語

1

では
$)$

$\mathrm{i}\mathrm{m}\mathrm{n}arrow\infty$aならば$\mathrm{i}\mathrm{m}\mathrm{n}arrow\infty \mathrm{b}\mathrm{n}=\mathrm{q}$$(\mathrm{P}\mathrm{r}\mathrm{f}\mathrm{D}\mathrm{L})$$\mathrm{D}a\ovalbox{\tt\small REJECT}$という関係ないし述語を、 1$\mathrm{n}=\mathrm{p}$で書き表す。 この言語

tends to $\inf$ ,$\mathrm{i}\mathrm{m}(\mathrm{n}$$[\mathrm{a}, \mathrm{n}]$,$\mathrm{P}$という Prolog-like な述語で表す。 すると上の命題は、 次のように表される。

証明すべき命題$\mathrm{l}\mathrm{i}\mathrm{m}$(tends to $\inf$ ,$\mathrm{n}$implies
数列の極限$\mathrm{l}\mathrm{i}\mathrm{m}$($[\mathrm{a},$$\mathrm{n}$$\mathrm{n}]$p) and,tends to

ところで、 この$\mathrm{l}\mathrm{i}\mathrm{m}$($\inf$$\mathrm{N}$,$\lim$($\mathrm{n}$$[\mathrm{a}+\mathrm{b},$tends to $\inf$ ,$\mathrm{n}]$,$\mathrm{p}+\mathrm{q}$tends to $\inf$ ,$[\mathrm{b},$$\mathrm{n}]$

,

q)

).

$[\mathrm{A},$$\mathrm{N}]$P),とは、 実質的に何を意味するのかを、 定義してやらなければならない。

1

定義$\mathrm{i}\mathrm{m}$(tends to $\inf$ ,$\mathrm{N}$(sequence (any ($\mathrm{E}\mathrm{p}\mathrm{s}$,$\{[\mathrm{A}$Eps$\mathrm{e}\mathrm{x}\mathrm{i}_{\mathrm{S}}\mathrm{t}_{\mathrm{S}}(\mathrm{N}2$,, Nl] :$>0$$\mathrm{N}1=1$$[\mathrm{A},$$\mathrm{N}]$,P) equiv

to inf} ) and real number{$[\mathrm{A}$, Nl]:

natural number(N2) and$\mathrm{N}1=1$についての通常の) andimpliesany (Ns, natural number (Ns) and Ns
つまり$(\mathrm{P})$N2 implies abs$([\mathrm{A}$

, Nsl

–P)

$<$

EPs) $))$ .

to inf} は数列 (sequence) であるということ、 そして後は、 極限値$\epsilon-\mathrm{N}$

実数をベースにする$>$論法である。

この論理式では限量子が動く集合は 「実数」 である。 つまり実数の集合を初めから基礎にしている。 「自然数$arrow$

有理数$arrow$

デデキントの切断$arrow$実数」 という

階段を登っていたのでは日が暮れるからである。 これは $-$ つの選択事項である。

(2) 数列とは何かをコンピュータに教える

ここで 「

{a
$\mathrm{n}$:$\mathrm{n}=1$

to inf } が数列である」 という述語は何を意味するのだろうか。 数列とは何であるかをコンピュータに教えなければならない。 数列に対する普通のイメージはものであろう。 人間は柔軟にこの点々 「.

{a

1

a2

a3 . . . } という. . 」 を理解するが、 この想像力をコンビュー

141

タに持たせることは困難に思える。 我々の当座の (上の公式を証明するという) 目的のためには、$\mathrm{d}\mathrm{e}\mathrm{f}$inition of sequenceを次のように与えておけば十分であることが分かった。

これはほぼ、 数列とは自然数から実数への関数である、 という言い方にひとしい。 なお、

sequence (XX)
定義

とは、 [

sequence ($\{[\mathrm{A},$$\mathrm{X}\mathrm{X}$は数列である」 という述語を表す。

$\mathrm{N}1]:\mathrm{N}1=1-$

to inf} )equivname of sequence(A) andany (N2, natural number (N2) implies real number$([\mathrm{A}$, N2])).

ここで当然、 自然数とは何であるか、 を必要な範囲で規定しておかねばならない (略)また、 2 っの数列の和の数列とは如何なるものか、 を教えなければならない。 composite

sequence定義$\mathrm{A}+\mathrm{B}$を次のように定義する。

sequence ($\{[\mathrm{A},$$\mathrm{N}1]:\mathrm{N}1=1$

to inf} )and sequence (implies any (N3, natural number (N3) implies
さらに、

定義

$\mathrm{A}+\mathrm{B}$の形も数列の名前$([\mathrm{A}+\mathrm{B}$$\{[\mathrm{B},$$\mathrm{N}2]:\mathrm{N}2=1$

, N3]

$=$

$[\mathrm{A},$to inf} )$\mathrm{N}3]+[\mathrm{B},$$\mathrm{N}31)$).

name of sequence であることを規定しておく。

name of sequence(A+B), if name of sequence(A) and name of sequence(B).

しかし–殺に数列の和差積雨は,

再帰的に行なわれることを思えば、 この規則は Prolog

でプログラム化しておいた方がよい。

name of sequence$(\mathrm{A}+\mathrm{B})$:-name of sequence (A), name of sequence (B).

このとき次の補題が形式的に証明される (証明略)命題

sequence ($\{[\mathrm{A},$$\mathrm{N}1]:\mathrm{N}1=1$

implies sequence ($\{[\mathrm{A}+\mathrm{B}$to inf} ) and sequence (, N3] :$\mathrm{N}3=1$(3) 関数とその性質についての主張

うな箇所が出てくる。 「自然数つ$\mathrm{N}\geqq \mathrm{N}2$。

$\mathrm{N}1$.

$\{[\mathrm{B},$$\mathrm{N}2]:\mathrm{N}2=1$

to inf} )to inf} ).

今問題にしている公式では、 証明の途中に次のよ$\mathrm{N}2$のうち大きな方を$\mathrm{N}$とするなら、$\mathrm{N}\geqq \mathrm{N}1$

且である」 。日常言語によるこの表現を、 純形式的な枠組でとらえようとすると、 事はそれほど簡単ではない。 / ここには現れている。 そして上の文は、 その$\mathrm{N}$$\mathrm{N}=\mathrm{m}$

に対して

a

$\mathrm{x}$$(\mathrm{N}1.

$\text{「}\mathrm{N}\geqq \mathrm{N}1$\mathrm{N}2)$

且つ

という

$\mathrm{N}\geqq \mathrm{N}2$

“

関数” が

である」 という性質のあることを主張している。 つまり関数の導入と、 その関数の性質の主張が、 日常
言語によって行なわれており、 われわれはそれを直観的に了解している。 そういった直観的了解をちゃんと形式化してコンピュータに教えてやらなければならない。
関数をどう形式的に定義するかが問題となる。 関数は Prolog プログラムで与えればよい

。

142

のではなかろうか $-$ それもなるべ$\mathrm{N}=\max$

Prolog の論理プログラムとしての部分を使う。

$\langle$(Nl, N2) という関係は、 Prolog では maxp ($\mathrm{N}1$という述語で表される (Prolog, N2, N)という言語の特徴による) 。ここでこれら両者を結ぶ規則

maxp (Nl, N2, N) equiv$\mathrm{N}=\mathrm{n}\mathrm{a}\mathrm{x}$(Nl, N2).

が必要である。 これに関連して、 論理はいわゆる 「等号をもつ理論」 であるから、

定理(X$=\mathrm{Y}$) implies (Terml$=$

Term2),

if Term2
を$\mathrm{Y},$

Terml

は

の X, $Y$の現れのいくっかに置き換えたもの.

$\mathrm{X}$などの、 等号の公理や定理を設定しておかなければならない。

述語 maxP (Nl, N2, N) に対するプログラムは次のようになる。 これが関数の定義である。

maxp (Nl, N2, N) :- Nl $>=$ N2,

maxp (Nl, N2, N) :- Nl

$<$

N2,

NL

$\mathrm{N}=$$\mathrm{N}=$N2.

関数を Prolog プログラムで与えたとして、 それを論理で扱うには、 Prolog と論理とのイ
ンタフェイスあること、$\mathrm{A}$(接点) が必要になる。 これは簡単で、 Prolog の

:-B.

は

imples A であること$\mathrm{B}$$\text{、}$$\mathrm{A},$$\mathrm{B}$は論理の Aand

Prolog では不成功による$\mathrm{n}\mathrm{o}\mathrm{t}$$\mathrm{B}$

で

が採用され

ていること等を言っておけばよい。それを通して関数の性質を論理的に証明する。 例えば、
命題

maxp ($\mathrm{N}1$, N2, N)

implies ($\mathrm{N}>=$命題

maxp ($\mathrm{N}1$, N2. N)

implies ($\mathrm{N}=$

Nl)

and (

Nl)

or (

$\mathrm{N}>=$$\mathrm{N}=$

N2).

N2).

などの補題である。 これらは人間には自明だが、 機械には自明ではない。

(4) 実数の諸性質

実数は、 順序と代数と位相 (あるいは距離) の性質をもち、 それら

は、 等号や不等号に関する公式として表される。 証明チェッカとしては、 等号と不等号を含む式を導出する数式処理の能力をもっていることが望ましい。
デデキントの切断によって実数を定義したのならば、 実数の性質は本来、 自然数 (や有理数) の性質から証明されるべき事柄である。 しかし我々はいきなり実数から始めた。 その場合でも、 実数の性質を公理として立てて、 他の性質はそれから導出するのが適切なやり方である。 だが我々は時間の都合でそれもせずに、 実数に関して必要な公式は、 th ofreals としてあらかじめ与えた。 例えば次のような公式である。
andth of reals([$\mathrm{X}>Y$

th of reals([$\mathrm{X}1>\mathrm{x}2$

th of reals([.abs (X)$Y>=\mathrm{Z}$

and
$+$

implies$Y1>\mathrm{Y}2$$\mathrm{a}\mathrm{b}\mathrm{s}(\mathrm{Y})$$\mathrm{X}>\mathrm{Z}1$

implies$>=$).

$\mathrm{X}1+Y1>\mathrm{X}2\dagger \mathrm{Y}2$$\mathrm{a}\mathrm{b}\mathrm{s}(\mathrm{X}+\mathrm{Y})$

1).

]).

143

基本公式を与えてそのいくらかの変形はプログラムで与える,$\mathrm{X}>Y$との同$\mathrm{Y}<\mathrm{X}$–視、 Xand

と

$Y$

$Y$

and X の同–ということも少しはした。

視、 などである。 我々としては微積の数

式的な面よりも、 論理的な面により多くの興味をもった。

命題論理の諸公式

自然推論の立場からいえば、 命題論理の公式はすべて自然推論によって導出されるものである。 証明チェッカは命題論理の公式、 特に同値公式は、 その場で直ちに証明できるのが望ましい。 これについても、 必要な公式をあらかじめ与えた。

証明のプロセス

証明したい命題は、 条件部および結論部に、 述語証明のプロセスは、 条件部のを$\mathrm{l}\mathrm{i}\mathrm{m}$$\text{、}\mathrm{d}\mathrm{e}\mathrm{f}$inition of limit$\mathrm{l}\mathrm{i}\mathrm{m}$

equiv

の

をもっている。
の式の右辺で置

き換え、 それの any や exists を推論規則によって除去し、 途中によく知られた等式についての和をとり、 次いで any やof limit$\lim$のequiv$\mathrm{e}\mathrm{x}\mathrm{i}$sts を推論規則によって導入し、$\epsilon/2$$\mathrm{d}\mathrm{e}\mathrm{f}$の不initionの式の右辺の形を作って、 それを左辺の式に置き換えて、 結論部のを作りだすことで終わる。 証明は補題を含め行数にして約 350 行かかった。

関数の極限値と$\epsilon-\delta$

論法

以上は数列の極限値に関する命題の$\epsilon-\mathrm{N}$論法による証明

を形式的化するものであったが、 他にわれわれは、 関数の極限値に関する同様な命題の$-\delta$

命題論法による形式的証明を実際に与えることができた (これは山下による)$\lim$($\mathrm{x}$tends to a,

implies 1
つまり、1$\mathrm{i}\mathrm{m}$($\mathrm{x}$$\mathrm{i}\mathrm{m}$$[\mathrm{f},$$\mathrm{x}]$P) and,tends to a,$\mathrm{f}$(X)$\lim$$[\mathrm{f}+\mathrm{g},$$=\mathrm{P}$$\mathrm{X}]$且つ$\mathrm{x}arrow \mathrm{a}$1($\mathrm{i}\mathrm{m}$$\mathrm{f}$(x)$+\mathrm{g}$(,tends to a,$\mathrm{x}$$\mathrm{p}+\mathrm{q}$1$[\mathrm{g},$$\mathrm{x}]$$\epsilon$

。

q)

,

).

$\mathrm{i}\mathrm{m}$(x) )$\mathrm{g}$(X)$=\mathrm{q}$ならば$\mathrm{x}arrow \mathrm{a}$$=\mathrm{P}+\mathrm{q}$$\mathrm{x}arrow \mathrm{a}$である、という命題である。 // 今、 「中間値の定理」 の形式的証明を作ろうとしている。 まだ最後までできていないが、 大体うまくゆくようである。

\S$\mathrm{m}$証明記述言語$\mathrm{P}\mathrm{r}\mathrm{f}\mathrm{D}\mathrm{L}$と証明チェッカ$\mathrm{P}\mathrm{r}\mathrm{f}\mathrm{C}\mathrm{h}\mathrm{e}\mathrm{C}\mathrm{k}\mathrm{e}\mathrm{r}$の実現論理系としては Genzen の提案した自然推論が人間の推論に近いものとして適当と思われる。 われわれの証明記述言語$\mathrm{P}\mathrm{r}\mathrm{f}\mathrm{D}\mathrm{L}$は、 ほとんど文献 [4]における$\mathrm{N}\mathrm{Q}$による証明の記法そのものである。 始めに命題を書く。 証明の各行は次のような形をしている。
[Label,Logical Formula,[Inference,$\mathrm{U}\mathrm{s}\mathrm{e}\mathrm{d}\iota \mathrm{a}\mathrm{b}\mathrm{e}\mathrm{l}\mathrm{l}$,$\mathrm{u}_{\mathrm{S}\mathrm{e}}\mathrm{d}\mathrm{L}\mathrm{a}\mathrm{b}\mathrm{e}12]$].

どの論理式とどの論理式から、 推論規則 Inference を用いて、 本論理式 Logical Formulaを導く、 というふうに、 推論規則 Inferenceを明示するもので、 いわばアセンブリ言語

144のように原初的である。 具体例を書く と、[22.

$\mathrm{e}\mathrm{x}\mathrm{i}_{\mathrm{S}}\mathrm{t}_{\mathrm{S}}(\mathrm{n}$

any (
(ns

$\mathrm{n}\mathrm{s}$natural number(n) and,natural number(ns) and,$>\mathrm{n}$) implies ([implies

改良版[3,$\mathrm{P}\mathrm{r}\mathrm{f}\mathrm{D}\mathrm{L}$$\mathrm{e}\mathrm{l}\mathrm{i}\mathrm{m}\mathrm{i},$$\mathrm{a}\mathrm{b}\mathrm{s}$($19,21$ ]$[\mathrm{a},$$]$$\mathrm{n}\mathrm{s}]$-p)$<\mathrm{e}\mathrm{p}\mathrm{s}/2$) $))$ ,.

では推論規則を明示しながらではあるが、 何ステップかの暗算ができる :cont inuous ($\mathrm{f}$at X on closed interval$(\mathrm{a},$$\mathrm{b})$), [[$\mathrm{j}1$. def inition of cont[j2, equiv elimi, 2,[j3, any elimi$\mathrm{j}1$inuous],],us ing term X,$\mathrm{j}2$

]

$]$

.

証明は、 始めから終わりまで書き下して、 ファイルに入れておく。 証明チェックは $-$ 応

バッチ式に行なわれるが、 証明ミスに対して対話式に正しい式を入力することも可能だ。
次に、 我々の証明チェッカ$\mathrm{K}$-Prolog)$\text{、}$$\mathrm{P}\mathrm{r}\mathrm{f}\mathrm{C}\mathrm{h}\mathrm{e}\mathrm{C}\mathrm{k}\mathrm{e}\mathrm{r}$について述べる。 実現言語は Prolog (具体的には使ったマシンは SUN の SPARK IPX である。 チェッカは証明の各行に対して、

正しい推論がなされているか、 特に限量記号 any や exists の導入や除去に際しての付帯条件が満たされているか否か、 を調べ、 その行の論理式が従属する仮定をメモしてゆく。 ミ
スがあればメ ッセージを出して止まるか、 または正しい論理式の入力を求める。 よくある
ミスは、 付帯条件に言うところの 「自由」 という条件である。 / 最後に end of$\mathrm{f}$ile にくれば、 始めの命題と最後の行の $-$ 致を見、 すべての仮定が除去されているかを調べ、 正し

ければ簡単な証明木を出力し Congratulation !! と書いて終わる。
われわれのプログラミングでは、 チェッカの作成と (数列の命題の) 証明の作成とは互いのエラーを指摘しあうという形で平行して行なわれ、 それにより両者のデバッグがうまくできた。 要した時間は見当で延べにして、 チェッカの作成に約 70 時間、 (数列の命題の)証明の作成に約 50 時間く らいである。 チェッカの作成に難しいことは特に何もない。 形式的証明の作成の方が、 よりクリエイティ ブな工夫を要するものでやや難しい所があった。

\S IV

終わりに

–

評価と提言

数列の命題に関して、 形式的証明は確かに存在した。 微積のテキストに書かれている証
明から、 その形式的証明を作るのは、 けっして自明ではなく、 ある程度の工夫を要するい

くらか難しい問題であった。 しかし有限的な形式的証明の根本的な功績は$-\delta$$\epsilon-\mathrm{N}$論法や$\epsilon$

論法にある。 この論法の偉大さに比べれば、 形式的証明に要した工夫は、 価値が小さ145

い。 / それでもなお、 微積のテキストを完全に形式化するという課題は‘教育的な価値’がある。 大学の教養課程の学生が数学を学び理解する際に、 数式処理的な側面以上に大事なのは論理的な理解である。 数式処理に対しては数式処理ソフトとして麗 athemat ica や盟 a$\mathrm{p}\mathrm{l}\mathrm{e}$等があるけれど、 それらに対応して、 それらと同程度に扱いやすい論理処理ソフト

例えばいて$\mathrm{L}\mathrm{o}\mathrm{g}\mathrm{i}\mathrm{c}$a とでもいうような名前の––があることが望まれる。 そんなソフトを用[コンピュータに数学を教える」 という数学学習法がありうる‘–

教えることが最上の学習法である’ という言葉が正しいならば。 / 次のようにまとめられる。
(1) 論理の取扱いという点で、 現在、 人間とコンピュータとの間にはギャップがある。

このギャップは、 人間とコンピュータの双方からの歩み寄りで解消されるべきである。
(2) 「コンピュータの側から人間への歩み寄り」–

これは証明記述言語の高級化、 というテーマとなる。 他方、 「人間の側からコンピュータへの歩み寄り」 $-$ これは数学の形式

化、 という研究テーマとなる。 現在は、 これら両面からのアプローチが必要であろう。
(3) それでもなおかっ数学に関して、 人間とコンピュータとの間のギャップは、 本質的で越えがたいものがあるように見える。 このギャップを埋めようという試みは、 究極的には、 人間の数学的能力そのものの AI 的研究、 というテーマにまでつながる。

いま数学にとって大事なのは、 数学それ自体の研究と同時に、 数学者が何故数学ができるのかの研究、 数学的あるいは論理的思考能力のメカニズムは何かの研究である。 そのテ$-$

マに、 ここでいう 「教育用研究」 は関連をもつ。

\S 参考文献[1] 高橋英之、 [『論語』 の公理化 $=>$ 孔子の AI 化へ」$\text{、}$

人工知能学会全国大会論文集、

1993, 7。
[2]

G. Takeuchi, ’Two Applicat ions of Logic to Mathemat,$\mathrm{i}\mathrm{c}\mathrm{s}’$[3] 萩谷昌己、 「証明チェッカとそのユーザインタフェ $-$ ス」$\text{、}$Iwanami,1978.

人工知能学会誌、 Vol. 10,

NO. 1, 1995 年 1 月。 これにかなり詳しい文献がついている。 なお、 次の文献も参照。
南俊朗、 沢村$-\text{、}$[対話型論証支援システム」$\mathrm{E}\mathrm{U}0\mathrm{D}\mathrm{n}\mathrm{I}\iota \mathrm{o}\mathrm{S}$$\text{、}$

人工知能学会誌、Vol. 5, NO. 1, 1990 年 1 月。
A. Quaife, ’Automated Development of Fundamental Mathematical Theories’,
KLUWER ACADEIIC PUBLISEERS, 1992.
[4] 安井邦夫、 『現代論理学』[51 L. Sterling$\text{、}$

世界思想社、 1991。

&E. Shapiro, lProlog の技芸』 (松田訳) , 共立出版、 1986。