JPH06314200A - 証明構築支援装置 - Google Patents

Abstract

(57)【要約】 【目的】 計算機による証明構築の支援処理に関し、原
論理式における変数の出現位置を示すテンプレートの候
補を自動的に生成して論理式の指定を支援する証明構築
支援装置を目的とする。 【構成】 論理式に対する導出規則を適用する支援処理
部１は、入力した論理式が所要の項を代入した式であ
り、該導出規則の適用結果として原論理式を必要とする
場合に、テンプレート選択部２に要求して、該テンプレ
ート選択部が返す論理式を該原論理式として処理し、テ
ンプレート選択部２は、該論理式の自由変数の代入結果
であることが可能な１個以上の項を自由変数の位置とし
て示し、異なる自由変数位置の組合せを持つテンプレー
トを生成して、該生成したテンプレートから１個の該テ
ンプレートを選択する入力を受け、該論理式の該入力に
より定まるテンプレートで示す項の位置を自由変数にし
た論理式を生成して支援処理部１に返すように構成す
る。

Description

【発明の詳細な説明】

【０００１】

【産業上の利用分野】本発明は、計算機を利用して、利
用者の証明構築作業を支援するための、証明構築支援装
置に関する。

【０００２】

【従来の技術と発明が解決しようとする課題】利用者が
例えば或る前提の式から或る結論の式が導かれることを
示す証明を、適当な導出規則を逐次適用することによっ
て構築しようとする場合に、そのような証明構築作業等
を計算機の処理によって支援することが考えられてい
る。

【０００３】証明は公知のように、必要な式や、証明過
程の情報である証明断片、及び必要な公理、定理等に導
出規則等を適用して結果を求めることにより、証明の各
１ステップが進められる。ここで、導出規則とは、例え
ば推論規則、書換え規則、派生規則等である。

【０００４】推論規則は、式全体に適用するもので、前
提から結論を導くものであり、図２(a）のように示され
る。図でB1、B2等は、それぞれ前提の式、Ｃはそれらの
前提に或る推論規則を適用することによって得られる結
論の式である。

【０００５】図２(b) は各前提Biが仮定Aij等(大括弧で
括り１組の仮定を表す）に基づいて得られる場合の推論
規則の形式であり、図２(c）は書換え規則の形式を示
す。これらの導出規則を「適用」するとは、利用者が指
定する式を構文解析して、所要の条件を満足する論理式
であれば、導出規則における前提或いは書換え前の表現
と、その式とのパターンマッチングを行い、パターンが
一致したときに、結論或いは書換え後の表現を導く処理
である。

【０００６】このような証明構築の支援装置では、前記
の操作で指定された導出規則を適用して結果を求める処
理を行うと共に、利用者が導出規則を指定する操作を容
易にするために、すべての導出規則を表示して、その中
から利用者に選択させたり、又は、利用者が入力した式
や証明断片等の範囲内で、適用可能な導出規則の候補を
表示して選択させることによって支援している。

【０００７】ここで、図２(d)に示す推論規則∃の導出
規則は、「Ｐ(t/x)が証明されれば、∃x.Ｐ(x)(即ち、
Ｐ(x)を真とするｘが存在する)ことを証明できる」こと
を示す。但し、Ｐ(t/x)は論理式Ｐ(x)の自由変数ｘに項
ｔを代入した論理式である。

【０００８】従って、例えば「０＝０＋０」という論理
式が与えられ、ｔを０として導出規則である推論規則∃
の導出規則を適用しようとすると、先ずＰ(0/x）は一般
的な論理式を示すから０＝０＋０と無条件にマッチング
が得られる。

【０００９】そこで導出規則に従って結論を表すため
に、Ｐ(x）を知る必要があるが、代入して０＝０＋０に
なる、もとの論理式（原論理式とする）は０＝ｘ＋０で
あってもｘ＝ｘ＋ｘであってもよく、その他変数の出現
位置の各種組合せが可能であるので、結論が定まらな
い。

【００１０】従ってこのような場合に証明を続けるため
には、利用者が原論理式を指定しなければならず、指定
の方法としては、例えば変数の出現位置を左から数えあ
げる方法、論理式の構文解析による構文木の各枝に番号
を付け、構文木上の位置をルートからたどる枝の番号列
で表すようにした自然数のリストで、構文木上の変数の
出現位置を与える方法、代入後の論理式と原論理式を共
に入力する方法等がある。

【００１１】しかし、以上の何れの方法でも、論理式が
複雑になると共に、入力が煩雑となり、入力の誤りの発
生も多くなる。本発明は、前記のような場合に原論理式
における変数の出現位置を示すテンプレートの候補を自
動的に生成して、論理式の指定を支援する証明構築支援
装置を目的とする。

【００１２】

【課題を解決するための手段】図１は、本発明の構成を
示すブロック図である。図は証明構築支援装置の構成で
あり、論理式と導出規則を入力して、該論理式に対する
該導出規則の適用を判定し、適用可能な該導出規則に従
って、該論理式に対応する適用結果を生成する支援処理
部１を有する証明構築支援装置であって、テンプレート
選択部２を設ける。

【００１３】支援処理部１は、該入力した論理式が原論
理式の自由変数に所要の項を代入した式であり、該導出
規則の適用結果として該原論理式を必要とすることを識
別した場合に、テンプレート選択部２に該入力した論理
式を渡して、該テンプレート選択部が返す論理式を該原
論理式として処理する。

【００１４】第１の発明では、テンプレート選択部２
は、該論理式の自由変数の代入結果であることが可能な
位置を自由変数の位置として示し、異なる自由変数位置
の組合せを持つテンプレートを生成して、該生成したテ
ンプレートから１個の該テンプレートを選択する入力を
受け、該論理式の該入力により定まるテンプレートで示
す位置を自由変数にした論理式を生成して支援処理部１
に返す。

【００１５】第２の発明では、前記テンプレート選択部
２は、前記選択の最初に複数の前記テンプレートのうち
から所定の条件によって選択する該テンプレートを示
し、当該テンプレートを選択するか否かの入力を受け
る。

【００１６】

【作用】本発明の証明構築支援装置により、証明構築等
の支援処理において、自由変数に代入を行った論理式に
導出規則を適用するために、原論理式を定める必要があ
る場合には、支援装置が自動的に原論理式の自由変数の
位置を示すテンプレートを生成し、利用者に対し表示等
して、その中から一つのテンプレートを選択させる。

【００１７】従って、利用者は原論理式そのものを入力
したり、論理式の自由変数の位置を指定する入力をした
りする必要が無く指定して、必要な原論理式の指定を容
易且つ確実に行うことができる。

【００１８】

【実施例】図３は、本発明の証明構築支援装置の処理の
流れの一例を示す図であり、図は例えば利用者から指定
された論理式を入力し、例えば利用者が指定したり、或
いは別途支援装置が自動的に選んだ導出規則を、その論
理式に適用する場合の処理を示すものである。

【００１９】図３において、先ず図１の支援処理部１が
処理ステップ10で論理式と導出規則を取り出すと、処理
ステップ11で構文解析を行い、処理ステップ12で構文解
析結果を識別して、論理式としての要件を満足していな
ければ導出失敗として、今回の適用処理を終わる。

【００２０】構文解析に成功すれば、処理ステップ13で
導出規則の条件部分とのパターンマッチを行い、処理ス
テップ14でパターンマッチの成否により、この導出規則
の適用可否を識別して、適用不可なら今回の処理は導出
失敗として終了する。

【００２１】導出規則が適用可であれば、支援処理部１
は処理ステップ15で、この論理式が代入のある式であ
り、且つ導出規則の適用のために原論理式を知る必要が
あるかを、現に使用する導出規則から識別し、その結果
そのまま導出規則の適用を進められる場合には、処理ス
テップ19に進んで適用処理を行う。

【００２２】原論理式を知る必要がある場合には、支援
処理部１はテンプレート選択部２に処理を要求する。そ
こでテンプレート選択部２は処理ステップ16で、その論
理式に基づいてテンプレートを作成する。

【００２３】テンプレートの作成処理では、Ｐ(t/x)に
相当する論理式を構文解析して、構文上自由変数ｘが出
現できる位置を識別し、その条件に該当するすべての位
置の中の０個以上の位置を所定のプレースホルダー記号
で置き換え、置換しない位置は代入値ｔのままとして１
個のテンプレートとし、プレースホルダー記号への置換
位置の異なるすべての場合についてテンプレートを作成
する。

【００２４】従って、例えば前記例のように、論理式０
＝０＋０に、導出規則として推論規則∃の導出規則を適
用する例では、図４に示すように８個の異なるテンプレ
ートが生成される。なお、図では「$$」をプレースホル
ダー記号としている。

【００２５】次にテンプレート選択部２は、処理ステッ
プ17でテンプレートを表示装置に表示して、利用者に選
択を促し、選択入力を待つ。そこで、利用者は例えば表
示画面上のカーソルを所要のテンプレートの表示位置に
動かして指定キーを押す等の操作によりテンプレートを
選択する。或いは各テンプレートに番号を付けて表示
し、利用者は選択するテンプレートの番号を入力する。

【００２６】又、第２の発明により、一定の条件を満足
するテンプレート、例えば式の左から数えて最初の自由
変数出現位置をプレースホルダーにしたテンプレート、
或いは出現位置をすべてプレースホルダーにしたテンプ
レート等を、いわゆるデフォルトとして先ず作成して表
示するようにする。

【００２７】それに対して、利用者はデフォルトのテン
プレートを採択するか否かのみを、例えば所定の１キー
入力で示し、テンプレート選択部２は否の入力の場合の
み、その他のテンプレートを前記のように作成し表示し
て利用者に選択させる。

【００２８】このようにすることにより、選択の可能性
の高いテンプレートについて、利用者の指定を更に容易
にし、又、処理を早く進めることができる。利用者がテ
ンプレートを選択する入力を行うと、テンプレート選択
部２は選択されたテンプレートのプレースホルダー記号
で示される位置を自由変数にした論理式を作成して支援
処理部１に返すので、支援処理部１は処理ステップ19
で、その論理式を原論理式として導出規則を適用する処
理を行う。

【００２９】その結果、図４に例示する各テンプレート
が指定された場合に、推論規則∃の導出規則を適用し
て、それぞれその右に示す推論結果を生成することがで
きる。以上の説明で使用したプレースホルダーの記号
は、予めシステムで定める記号のみを使用しても、シス
テムで定める記号をデフォルトとして、利用者が任意の
記号を指定できるようにしても、常に利用者が指定する
ようにしてもよい。

【００３０】そのように利用者の指定を可能にすること
は、システムの定めた記号が既に論理式中に存在する場
合に混同を避ける等のために有効である。又、以上の説
明では、原論理式の指定を必要とする場合には常にテン
プレートの候補を作成して利用者に選択させるようにし
たが、例えば支援処理部１が前記図４の処理ステップ15
で原論理式を必要と判定した場合に、直ちに利用者に原
論理式を入力するか否か問い合わせるようにしてもよ
い。

【００３１】そこで利用者が原論理式を入力するか、或
いは原論理式における自由変数の出現位置を指定する等
の入力を行えば、支援処理部は、その入力で定まる論理
式が導出規則の適用に原論理式として使用可能かチェッ
クし、妥当な論理式であればテンプレート選択部２に処
理を要求することなく、その式を使用して処理を進め
る。

【００３２】又、問い合わせに対し、それをパスするこ
とを示す適当なキー入力があった場合には、テンプレー
ト選択部２に前記と同様の処理を要求するようにする。
このようにすることにより、比較的簡単な論理式が対象
になっている等の場合に、テンプレートを選択するよ
り、むしろ利用者が直接原論理式を指定して、作業を迅
速に進めるようにすることができる。

【００３３】

【発明の効果】以上の説明から明らかなように本発明に
よれば、計算機による証明構築等の支援処理に関し、代
入のある論理式に対する原論理式の指定を必要とする場
合に、原論理式における変数の出現位置を示すテンプレ
ートの候補を自動的に生成して論理式の指定を支援する
ので、証明構築等の作業を効率よく進めることができる
という著しい工業的効果がある。

【図面の簡単な説明】

【図１】 本発明の構成を示すブロック図

【図２】 導出規則の形式例を示す図

【図３】 本発明の処理の流れ図

【図４】 テンプレート例を説明する図

【符号の説明】

１ 支援処理部 ２ テンプレート選択部 10〜19 処理ステップ

Claims (2)

【特許請求の範囲】
1. 【請求項１】 論理式と導出規則を入力して、該論理式
   に対する該導出規則の適用を判定し、適用可能な該導出
   規則に従って、該論理式に対応する適用結果を生成する
   支援処理部(1)を有する証明構築支援装置であって、 テンプレート選択部(2)を設け、 該支援処理部(1）は、該入力した論理式が原論理式の自
   由変数に所要の項を代入した式であり、該導出規則の適
   用結果として該原論理式を必要とすることを識別した場
   合に、該テンプレート選択部(2）に該入力した論理式を
   渡して、該テンプレート選択部が返す論理式を該原論理
   式として処理し、 該テンプレート選択部(2）は、該論理式の自由変数の代
   入結果であることが可能な位置を自由変数の位置として
   示し、異なる自由変数位置の組合せを持つテンプレート
   を生成して、該生成したテンプレートから１個の該テン
   プレートを選択する入力を受け、該論理式の該入力によ
   り定まるテンプレートで示す位置を自由変数にした論理
   式を生成して該支援処理部(1）に返すように構成されて
   いることを特徴とする証明構築支援装置。
2. 【請求項２】 前記テンプレート選択部(2）は、前記選
   択の最初に複数の前記テンプレートのうちから所定の条
   件によって選択する該テンプレートを示し、当該テンプ
   レートを選択するか否かの入力を受ける、請求項１記載
   の証明構築支援装置。