JPH05224938A - 適用条件処理装置 - Google Patents

Abstract

(57)【要約】 【目的】 基本的な適用条件を組み合せて適用条件を容
易に表現する。 【構成】 推論規則や公理の適用条件の基本となる適用
条件を適用条件記憶部１に格納しておき、適用条件設定
部２で扱う推論規則や公理ごとに基本となる適用条件を
取り出し組み合せて対応付ける。証明実行部３でこれに
より推論規則を使って証明を行うときは、この推論規則
に対応付けられた適用条件が満足されているときのみ証
明を進めることができる。また公理を使って証明を行う
ときには、対応する適用条件を満足するときのみ、その
公理を使用することができる。

Description

【発明の詳細な説明】

【０００１】

【産業上の利用分野】本発明は、作成した証明に間違い
がないか否かチェックする証明チェッカや証明を作成す
るツールである証明コンストラクタにおいて、証明に使
用する推論規則や公理に用いる適用条件の正当性を確認
する適用条件処理装置に関する。

【０００２】

【従来の技術】証明チェッカや証明コンストラクタにお
いて、推論規則を適用して証明を行う際に、証明ステッ
プの正当性を保証するため、その推論規則に付けられて
いる適用条件を満たした場合だけ証明を進めることが要
求される。このため、推論規則ごとに適用条件を記述
し、推論規則を使った証明を行う際に適用条件をチェッ
クする機能が必要である。公理の場合も同様に適用条件
を満足した公理だけを証明で用いることが要求される。

【０００３】従来は推論規則や公理の適用条件を表わす
のに、適用条件の持つ意味を特別な意味記述言語（論理
を記述するためのプログラミング言語）を用いて間接的
に表わしていた。

【０００４】

【発明が解決しようとする課題】このため、このような
従来の記述方法では次のような問題を生じていた。 予備知識の問題 上述の意味記述言語を知らないと適用条件が書けないた
め、時間をかけて複雑な言語を学習する必要がある。 記述の容易さの問題 どのような推論を行う規則なのかを記述するときに、そ
の一部として適用条件も記述することになるため、誤っ
た記述を行う可能性が高い。

【０００５】すなわち、従来の記述方法は、基本的には
専門家向けの記述方法であり、初心者、意味記述言語を
知らない人などの一般の人が記述するにはかなり困難で
あった。

【０００６】本発明は上述の問題点に鑑みてなされたも
ので、様々な論理に現れる基本的な適用条件を抽出し、
適用条件の持つ意味を基本的な適用条件を組み合せて直
接的に表現する適用条件処理装置を提供することを目的
とする。

【０００７】

【課題を解決するための手段】図１は本発明の第１原理
図である。本発明の適用条件処理装置は、推論規則に適
用する適用条件を記憶する適用条件記憶部１と、推論規
則を格納し使用する推論規則について前記適用条件記憶
部１より必要とする適用条件を選択し使用する推論規則
とその適用条件の組み合せを設定する適用条件設定部２
と、この使用する推論規則を適用して証明を行う際に、
この使用する推論規則と選択した適用条件の組み合せが
満足するものであるか否かの確認を行う証明実行部３と
を備えたものである。

【０００８】また、前記証明実行部３は、前記推論規則
と選択した適用条件の組み合せが満足するものであるか
否かの確認を証明完成後でなければできない場合は、証
明完成後に確認するようにしたものである。

【０００９】図２は本発明の第２原理図である。本発明
の適用条件処理装置は、推論規則に適用する適用条件を
記憶する適用条件記憶部１と、推論規則に適用する適用
条件を作成する適用条件作成部４と、推論規則を格納し
使用する推論規則について前記適用条件記憶部１、前記
適用条件作成部４より必要とする適用条件を選択して使
用する推論規則とその適用条件の組み合せを設定する適
用条件設定部２と、この使用する推論規則を適用して証
明を行う際に、この使用する推論規則と選択した適用条
件の組み合せが満足するものであるか否かの確認を行う
証明実行部３とを備えたものである。

【００１０】また、前記証明実行部３は、前記推論規則
と選択した適用条件の組み合せが満足するものであるか
否かの確認を証明完成後でなければできない場合は、証
明完成後に確認するようにする。

【００１１】また、公理に適用する適用条件を記憶する
適用条件記憶部１と、公理を格納し使用する公理につい
て前記適用条件記憶部１より必要とする適用条件を選択
し使用する公理とその適用条件の組み合せを設定する適
用条件設定部２と、この使用する公理を適用して証明を
行う際に、この使用する公理と選択した適用条件の組み
合せが満足するものであるか否かの確認を行う証明実行
部３とを備えたものである。

【００１２】また、公理に適用する適用条件を記憶する
適用条件記憶部１と、公理に適用する適用条件を作成す
る適用条件作成部４と、公理を格納し使用する公理につ
いて前記適用条件記憶部１、前記適用条件作成部４より
必要とする適用条件を選択し使用する公理とその適用条
件の組み合せを設定する適用条件設定部２と、この使用
する公理を適用して証明を行う際に、この使用する公理
と選択した適用条件の組み合せが満足するものであるか
否かの確認を行う証明実行部３とを備えたものである。

【００１３】

【作用】上記構成により、適用規則や公理の適用条件の
基本となる適用条件を適用条件記憶部１に格納してお
き、適用条件設定部２で、扱う推論規則や公理ごとに基
本となる適用条件を取り出し組み合せて対応付ける。こ
れにより推論規則を使って証明を行うときは、この推論
規則に対応付けられた適用条件が満足されているときの
み証明を進めることができる。また、公理を使って証明
を行うときは、対応する適用条件を満足するときのみそ
の公理を使用することができる。

【００１４】適用条件記憶部１に格納されている基本と
なる適用条件だけでは適用条件を十分に表わせないとき
には、適用条件作成部４によって作成した適用条件を追
加することによって実現する。

【００１５】また、推論規則の適用条件については、証
明が完成されたときにしかチェックができない適用条件
があるので、証明途中でのチェックを保留し、証明完成
時にチェックを行うことにより、適用可能な証明スタイ
ルの範囲を広げることができる。

【００１６】

【実施例】以下、本発明の実施例を図面を参照して説明
する。図３は本発明の第１実施例の構成を示す図で、図
１に示す原理図１の具体例を示す。図１における適用条
件記憶部１に記憶されている適用条件として、図３に示
すように４つの条件を設ける。

【００１７】４つの条件の意味は次の通りである。 T is free for X in P：論理式 Pの中の変数X に項T を
代入したとき、項T の中で自由変数であったものは、や
はり自由変数である。 T is bound in P ：論理式P の中で変数T は束縛変数で
ある。 T is not free in P：論理式P の中で変数T は自由変数
でない。 A is an eigen-variable：項A はeigen-variableであ
る。 template：menu：論理式P の中の変数に代入を行うと
き、代入の対象とする変数はユーザが指定する。

【００１８】証明チェッカや証明コンストラクタにおい
ては、推論規則用の適用条件として、次の４つの条件を
設ける。 自由変数であること 束縛変数であること 自由変数でないこと eigen-variableであること

【００１９】そして上記４つの条件の中から使用する推
論規則に適用する条件を選択し、この選択した適用条件
を全て満足するように証明を進める。

【００２０】公理の適用条件としては、，，の中
から選択するようにする。これはのeigen-variableの
チェックは、証明を進めていって導かれた論理式に対し
て行うものであり、公理のように、それを導くのに仮定
している論理式のない論理式に対しては不用となるから
である。

【００２１】上述の適用条件によって大部分の論理で使
われる推論規則や公理の適用条件はカバーできる。しか
し、新たな適用条件が必要な場合もあり、図２の発明の
原理２に示すように適用条件作成部４を設けて対応す
る。

【００２２】図１，２に示す適用条件設定部２は、使用
する推論規則または公理に対して適用条件記憶部１の上
述した４個または３個の適用条件の内から選択する。図
３に示す例は述語論理の推論規則∃Ｅの適用条件を示し
たもので、この推論規則の適用条件は、選択された適用
条件の３つを全て論理積（and ）で結合したものであ
る。適用条件設定部２として、専用エディタを用いてい
る。

【００２３】ここで証明に使われる推論規則および書換
え規則について説明する。推論規則は、図４（ａ）に示
すパターンで示され、線の上にある論理式から線の下に
ある論理式を得ることができることを示している。仮定
式はあってもなくてもよい。仮定式ｉと前提式ｉをつな
ぐ「：」は、前提式を導くための仮定の１つに仮定式ｉ
があるということを示している。

【００２４】証明の中で指定した仮定式と前提式と、推
論規則の定義の前提式と仮定式のパターンが一致し、か
つ、推論規則に適用条件が付いているならば、それを満
しているときに限り、結論式が導ける。推論規則に適用
条件が付いていないときは、証明の中で指定した仮定式
と前提式と、定義の前提式と仮定式のパターンが一致す
れば、結論が導ける。

【００２５】書換え規則は、（ｂ）に示すパターンで示
される。書換え前と後の式は、見た目は異なるが同じこ
とを表わす。推論規則は、論理式全体にしか適用できな
い。定義を見ると、線の上には複数個の式がきてよい。
のに対し、書換え規則は、論理式の中の一部分にも適用
可能である。

【００２６】定義を見ると線の上と下の式の数は必ず１
つである。

【００２７】図５は適用条件設定部２に格納する推論規
則の一例を示すメニューである。図６，図７は推論規則
の具体例を示す。上段に推論規則の名前を示し、中段に
推論規則、下段はこの推論規則に適用する適用条件を設
定するものである。図８，図９は書換え規則の具体例を
示す。書換え規則には適用条件はない。

【００２８】図10は述語論理の推論規則∃Ｅの適用条件
を設定する方法を説明する図である。同図において
（ａ）は専用エディタを示し、（ｂ）はこの専用エディ
タによって適用条件を指定した状態を示す。

【００２９】（ａ）の上段は、図３に示した４つの適用
条件が示されている。この中から、適用条件を過不足な
く指定するために専用エディタを設けてある。このエデ
ィタの一番上の領域はメニューで、各々の行のメニュー
の項目になっている。この項目の中で「＊」で括って示
されているものが適用条件を示すのに必ず必要な要素を
示す。例えば、自由変数を表すには、項目の中に「＊」
で括って示されているｔ（項１）、ｘ（変数）、P
（ｘ）（項２）の３つの要素が必要であることを示す。
また、eigen −variableであることを示すには、ａ
（項）が必要である。他の適用条件についても、同様で
ある。

【００３０】メニューの中の項目を一つ選ぶと、その下
の領域にプロンプトが出る。このプロンプトは、適用条
件を示すのに必要な要素の入力を要求するものである。
必要な要素を全て入力し終ると、その下のメニューに基
本となる適用条件が表示される。以上の動作を繰り返し
て、必要な適用条件をすべて入力すると、推論規則の適
用条件の定義が終る。推論規則に適用条件が付いている
時には、すべての適用条件をすべて満たした時にのみ、
その推論規則を適用することが許される。

【００３１】例えば、このエディタで、「変数Z は、項
Q の中で自由変数ではない。」という適用条件を定義す
るには、一番上のメニューの中の項目「＊ｘ＊ is not
freein ＊P （ｘ）＊」を選ぶ。そうすると、その下の
領域に「ｘ？＞」と、次に「P （ｘ）？＞」というプロ
ンプトが出る。各々に対して、「Z 」，「Q 」と入力す
ると、必要な要素が揃ったので、その下のメニューに適
用条件「Z is not free in Q」が表示される。

【００３２】このようにして指定した適用条件の意味は
次の通りである。 Z is not free in Q：論理式Q の中で変数Z は自由変数
でない。 Z is not free in ∃XP（X ）：論理式∃XP（X ）の中
で変数Ｚは自由変数でない。 Z is an eigen-variable：項Z はeigen-variableであ
る。 template：all-occurrence：論理式P の中の変数に代入
を行うときに、すべての変数を代入の対象とする。

【００３３】次に図３に示す証明実行部３について説明
する。証明実行部３は証明を行うが、証明に関する基本
的動作は次の３つである。 推論規則や書換え規則（これらをまとめて導出規則と
いう）の定義から、前提の論理式、仮定の論理式、結論
式のパターンを導出規則ごとに記憶する。 ユーザの入力する論理式を記憶する。公理や定理の論
理式が入力される場合もある。

【００３４】入力済の論理式の中から、ユーザが仮定
として指定した論理式、前提として指定した論理式と、
それらに適用する導出規定を取り出す。ユーザが指定し
た論理式に導出規則が適用可能ならば、適用して結論の
論理式を作成する。結論の論理式も入力された論理式と
同様に指定し、導出規則を適用することができる。

【００３５】ユーザの指定した論理式と、導出規則の定
義に書かれている前提の論理式、仮定の論理式のパター
ンが一致し、かつ、導出規則が推論規則ならば適用条件
を満足しているときに「適用可能である」と言い、適用
可能な時、導出規則の定義に書かれている結論の論理式
のパターンから結論の論理式を作成することを「導出規
則を適用する」と言う。導出規則を１回適用することを
証明を１ステップ進めると言う。

【００３６】証明実行部３では、作成した証明の保存
や、論理式の複写も行う。また、導出規則を適用すると
きに、前提と仮定から結論を得るのではなく、逆に結論
から前提を得る方法もある。

【００３７】図11は述語論理における適用条件のチェッ
ク例を示す。本図により適用条件のチェックを具体的に
説明する。図中Ａ〜Ｌは論理式に付けた符号である。以
下の説明は次のように分けて行う。 １．Ａの論理式の入力からＣの論理式を導くまで ２．Ａの論理式の複写（Ａ−copy）からＥの論理式を導
くまで ３．ＣとＥの論理式からＨの論理式を導くまで ４．Ｉの論理式の入力からＪの論理式を導くまで ５．ＨとＪの論理式からＬの論理式（結論）を導くまで

【００３８】１．Ａの論理式の入力からＣの論理式を導
くまで 仮定となる論理式（以降仮定式と称す） NANDGate（i1，i2，x ）∧NOTGate （x ，outp）…Ａ を入力する。仮定となる論理式には番号がつき、この場
合３となる。式Ａに図７（ｄ）に示す推論規則「∧Ｅ
Ｑ」を適用する。定義の前提式のパターンとＡ式は次の
ように一致している。

【００３９】Ｐに当るのは、NANDGate（i1，i2，x ） Ｑに当るのは、NOTGate （x ，outp）

【００４０】結論の論理式（以降、結論式と称す）のパ
ターンはＱなので、論理式、 NOTGate （x ，outp）…Ｂ を導く。この推論規則について、本実施例では適用条件
が付いていないので、適用条件のチェックは不用とな
る。なお、適用条件が付くか否かはユーザが指示する。
論理式Ａの下に線を引き、線の横には適用した推論規則
の名前と結論式が依存している仮定の番号３を中カッコ
で括って表示し、線の下には結論式を表示する。

【００４１】次にＢの論理式に図８（ｅ）に示す書換え
規則NOTGate def を適用する。書換え規則の定義と対
応することにより、 Ｐに当るのは、ｘ Ｑに当るのは、outp ということがわかる。書換え後の式のパターンはＱ≡〜
Ｐ（〜はnot を表わす)であるから、論理式、 outp≡〜ｘ…Ｃ を導く。論理式Ｂの下に線を引き、線の横には適用した
書換え規則の名前と、結論式が依存している仮定の番号
３を中カッコで括って表示し、線の下には結論式を表示
する。

【００４２】２．Ａの論理式の複写（Ａ−copy）からＥ
の論理式を導くまで この場合、推論規則として図７（ｃ）に示す∧ＥＰを適
用し、書換え規則として図８（ｆ）に示すNANDGate de
f を使うことにより１．と同様にＥの論理式を得ること
ができる。

【００４３】３．ＣとＥの論理式からＨの論理式を導く
まで ＣとＥの論理式に図６（ａ）に示す推論規則Ｒｅｐを適
用する。この場合、 Ｐに当るのは、outp≡〜ｘ Ｑに当るのは、ｘ Ｒに当るのは、〜（i1∧i2） ということになる。そして結論式のパターンはＰ（Ｒ／
Ｑ）であるので次の結論式が得られる。

【００４４】outp≡〜〜（i1∧i2）…Ｆ

【００４５】この推論規則も適用条件は不用とのユーザ
の指示があるものとし、適用条件のチェックは行なわな
い。論理式ＣとＥの下に線を引き、線の横には適用した
推論規則の名前と結論式が依存している仮定の番号３を
中カッコで表示し、線の下には結論式を表示する。

【００４６】次にＦの論理式の中の≡の右側の式に図８
（ｇ）に示す書換え規則〜〜Ｅを適用する。書換え規則
より Ｐに当るのは、（i1∧i2） ということがわかる。書換え後の式のパターンはＰであ
るから論理式は次のようになる。

【００４７】outp≡i1∧i2…Ｇ

【００４８】さらに、Ｇの論理式に、図９（ｈ）に示す
書換え規則ANDGate def0を適用する。 Ｐに当るのは、i1 Ｑに当るのは、i2 Ｒに当るのは、outp ということがわかる。書換え後の式のパターンはANDGat
e （Ｐ，Ｑ，Ｒ）であるから、次論理式を導くことがで
きる。

【００４９】ANDGate （i1，i2，outp）…Ｈ

【００５０】４．Ｉの論理式の入力からＪの論理式を導
くまで 仮定式ANDGate IMP （i1，i2，outp）…Ｉ を入力する。仮定となる論理式には番号10を付ける。式
Ｉに図９（ｉ）に示す書換え規則ANDGate IMP def
を適用する。 Ｘに当るのはi1 Ｙに当るのはi2 Ｚに当るのはoutp

【００５１】そして書換え後の式のパターンは、 ∃Ｔ（NANDGate（X ，Y ，T ) ∧NOTGate （T ，Z ）） であり、まだわからないＴをユーザに問い合せ、ｘとユ
ーザが入力したので論理は次のように導かれる。 ∃ｘ（NANDGate（i1，i2，x ）∧NOTGate （x ，outp））…Ｊ

【００５２】５．ＨとＪの論理式からＬの論理式（結
論）を導くまで ＨとＪの論理式に図10（ｂ）に示す推論規則∃Ｅを適用
する。 Ｐに当るのは、NANDGate（i1，i2，x ）∧NOTGate （x
，outp） Ｑに当るのは、ANDGate （i1，i2，outp） Ｚに当るのは、ｘ 結論式のパターンはＱであるから、次の論理式が導かれ
る。

【００５３】ANDGate （i1，i2，outp）…Ｋ

【００５４】推論規則の定義は、仮定式、前提式、結論
式のパターンを示すだけでなく、結論の依存する仮定に
ついても示している。例えば、推論規則∃Ｅを適用した
結果の結論式の依存する仮定については、「結論のＱが
依存する仮定とは、前提式∃ＸＰ（Ｘ）を導くための仮
定と、前提のＱを導くのに使われていた仮定のうちＰ
（Ｚ）以外のもの全ての合計である。」ということを示
している。故に結論のＱが依存する仮定は、10番の論理
式となる。

【００５５】次に、推論規則∃Ｅは次の３つの適用条件
を持っているので、これをチェックする。 ＺはＱの中で自由変数として現れない。 Ｚは∃ＸＰ（Ｘ／Ｚ）の中で自由変数として現れな
い。 Ｚはeigen-variableである。

【００５６】適用条件のチェック 論理式ANDGate （i1，i2，outp）の中にｘは現れていな
いので満足する。 適用条件のチェック 論理的∃ｘ（NANDGate（i1，i2，x ）∧NOTGate （x ，
outp）の中でｘは自由変数として現われていないので満
足する。 適用条件のチェック 結論の論理式が存在している10番の仮定ANDGate IMP
（i1，i2，outp）の中にｘが自由変数として現れていな
いので満足する。

【００５７】適用条件は全て満たされたので、この推論
規則は適用可能である。論理式ＨとＪの下に線を引き、
線の横には適用した推論規則の名前と結論式が依存して
いる仮定番号10を中カッコで括って表示し、線の下に結
論式Ｋを表示する。

【００５８】次にＩを仮定式（10番の付いた論理式）、
Ｋを前提式とし、それに図６（ｂ）に示す推論規則⊃Ｉ
を適用する。定義の仮定式と前提式のパターンＩ，Ｋか
ら、 Ｐに当るのは、ANDGate IMP （i1，i2，outp） Ｑに当るのは、ANDGate （i1，i2，outp） ということがわかる。そして結論式のパターンはＰ⊃Ｑ
であるので次の論理式を導くことができる。

【００５９】 ANDGate IMP （i1，i2，outp）⊃ANDGate （i1，i2，outp）…Ｌ

【００６０】推論規則⊃Ｉを適用した結果の結論式の依
存する仮定については、その定義から「結論のＰ⊃Ｑが
依存する仮定とは、前提式Ｑを導くための仮定のうちＰ
以外のもの全てである。」ということを示している。故
に、結論のＰ⊃Ｑが依存する仮定はなくなる。この推論
規則に対しては、ユーザは適用条件を付けていないもの
とする。論理式Ｋの下に線を引き、線の横には適用した
推論規則の名前と結論式が依存している仮定式がないこ
とを示すため、中カッコの中は空とし、線の下には結論
式Ｌを表示する。

【００６１】Ｌの論理式は、なんらの仮定なしに成り立
っている。このようなとき、論理式Ｌの証明が完成した
と言い、推論規則や書換え規則を適用してきた一連の流
れを論理式Ｌの証明と言う。

【００６２】なお、上述の実施例の証明を結論から行う
とeigen −variableのチェックができない。つまり論理
式ＫのANDGate （i1，i2，outp）と、推論規則∃Ｅから
線の上の２つの論理式ＪとＨ、∃ｘ（NANDGate（i1，i
2，x ）∧NOTGate （x ，outp），ANDGate （i1，i2，o
utp）を導く。このときにも適用条件のチェックを行
う。適用条件のうち次の２つは、上の３つの論理式Ｋ，
Ｊ，Ｈから可能である。

【００６３】論理式ANDGate （i1，i2，outp）の中で変
数ｘは自由変数でない。論理式∃ｘ（NANDGate（i1，i
2，ｘ）∧NOTGate （x ，outp）の中で変数ｘは自由変
数でない。

【００６４】しかし、項ｘがeigen-variableであること
は、線の下の論理式ANDGate （i1，i2，outp）が依存し
ている仮定の論理式がわからないのでチェックできな
い。適用条件に合っていないわけではないので証明が完
成して、論理式ANDGate （i1，i2，outp）が依存してい
る仮定の論理式がわかればチェック可能となる。

【００６５】推論規則を適用したときに、eigen-variab
leのチェックをせず、証明が完成した時に、証明を探索
してeigen-variableの適用条件が付いている推論規則が
あれば、その条件を満たしているかどうかチェックす
る。本例で言うと論理式ANDGate （i1，i2，outp）が依
存している仮定の論理式ANDGate IMP （i1，i2，out
p）の中で項ｘが自由変数でないことを確認する。

【００６６】なお、「Ｚはeigen-variableである」と
は、証明は、いくつかの仮定となる論理式から上述した
ように、推論規則等を何度も適用して行なわれるが、こ
のように証明を進めて行って導かれた論理式の依存して
いる全ての仮定の中にＺが自由変数として含まれない場
合をいう。

【００６７】また、∀ｘ．ｆ（ｘ，ｙ） 全てのｘについてｆ（ｘ，ｙ）が成立する。 ∃ｘ．ｆ（ｘ，ｙ） あるｘについてｆ（ｘ，ｙ）が成立する。 の∀ｘや∃ｘを限定作用素と言い、この限定作用素の作
用範囲は上の論理式で言うとｆ（ｘ，ｙ）となる。この
作用範囲の中のｘを「束縛変数」と言い、この作用範囲
の中の束縛変数でない変数ｙを「自由変数」という。

【００６８】また、推論規則∃Ｅは存在限量子∃（exis
t ）の削除（elimination ）の略で図３に示す∃ＸＰ
（Ｘ）という論理式は、「式Ｐを成り立たせるＸが存在
する。」という意味である。具体的な論理式を表わして
いるのではなく、この推論規則を適用できる論理式のパ
ターンを表わす。なお、図10に示すＰ（Ｘ／Ｚ）は論理
式Ｐ（Ｚ）の中のＺにＸを代入した式という意味を表わ
す。

【００６９】次に第２実施例を説明する。図12は本実施
例の構成を示し、図２に対応する。本実施例は適用条件
の１つeigen-variableを変更して新たな適用条件を作
り、その推論規則∃Ｅ’の適用条件の中の１つにしてい
る。適用条件作成部４としてテキスト・エディタを用い
ている。適用条件作成部４で作成した適用条件を、適用
条件記憶部２の専用エディタの中で他の適用条件と組み
合せている。

【００７０】図13，図14は適用条件作成部４のテキスト
・エディタによる新たなeigen −variableを作成してい
る状況を示し、図15はこれより図11に示す証明を変更し
た図である。新しい仮定式１，２が前の仮定式10にとっ
て代っている。

【００７１】新たな論理や推論規則を作成するときに、
基本となる適用条件だけでは表現できないような適用条
件が必要になったときには、新たな基本となる適用条件
を作成する。その適用条件の意味記述をテキスト・エデ
ィタで行う。意味記述はプログラミングに相当するもの
であるので、通常プログラミングに用いるテキスト・エ
ディタを本実施例では用いている。

【００７２】本実施例で推論規則∃Ｅの適用条件eigen-
variableの意味が、論理によって、次のように第１実施
例（図３）の場合と異なる。第１実施例の場合、eigen-
variableの条件は自由変数Ｚが次の条件を満たすことと
している。 前提式∃ＸＰ（Ｘ／Ｚ）の中で自由変数として現れな
い。 前提式Ｑの中で自由変数として現れない。 結論式Ｑの持つ仮定のうち、Ｐ（Ｚ）以外の全ての論
理式で自由変数として現れない。

【００７３】結論式Ｑの持つ仮定とは、前提式∃ＸＰ
（Ｘ／Ｚ）とＱの各々が持つ仮定の合計から、仮定Ｐ
（Ｚ）を除いたものであるから、を言い換えると次の
ようになる。 a 前提式∃ＸＰ（Ｘ／Ｚ）の依存している仮定式の中
では、Ｚは自由変数として現れない。 b 前提式Ｑの依存している仮定式のうち、Ｐ（Ｚ）以
外の論理式では、Ｚは自由変数として現れない。

【００７４】つまり、第１実施例で示したような通常の
eigen-variableの条件では、Ｚは２つの前提式の中で
も、２つの前提式が依存している仮定式（但し、Ｐ
（Ｚ）を除く）の中でも、自由変数であってはならな
い。

【００７５】これに対して、第２実施例で新たに作成し
たeigen-variableの条件は、，は全く同一である
が、が次のように異なっている。 ′Ｐ（Ｚ）を仮定に持つ論理式Ｑ（前提式Ｑ）の持っ
ている仮定のうち、Ｐ（Ｚ）以外の全ての論理式でも自
由変数ではない。そして前提式∃ＸＰ（Ｘ／Ｚ）の依存
している仮定については何も言っていない。つまり通常
のeigen-variableでのa がなくなっている。

【００７６】これは「２つの前提式の中と、前提式Ｑの
依存している仮定の中からＰ（Ｚ）を除いた仮定の中
で、Ｚは自由変数ではいけない。但し、前提式∃ＸＰ
（Ｘ／Ｚ）の依存している仮定式の中には自由変数とし
て現れてもよい。」と言い換えることもできる。

【００７７】第１実施例で示した通常のeigen-variable
適用条件と第２実施例で作成したeigen-variable適用条
件は、定数の名前替えを行えば、同じことを表してい
る。このように二つの表現があるのは、人によって条件
の表し方が異なるからである。

【００７８】上述の第１，第２実施例は、３つの適用条
件は∧（and ）で関連付けされていたが、or，if，whil
e などで組み合せてもよい。

【００７９】

【発明の効果】以上の説明から明らかなように、本発明
は、推論規則や公理の適用条件を基本的な適用条件の組
み合せによって実現できるため、適用条件を容易に作成
でき、証明の正当性を保証することに寄与するところが
大きい。また必要に応じて適用条件を新に作成すること
も可能である。

【図面の簡単な説明】

【図１】本発明の第１原理図である。

【図２】本発明の第２原理図である。

【図３】本発明の第１実施例を説明する図である。

【図４】推論規則と書換え規則のパターンを説明する図
である。

【図５】推論規則のメニュー例を示す図である。

【図６】推論規則例を示す図である。

【図７】他の推論規則例を示す図である。

【図８】書換え規則例を示す図である。

【図９】他の書換え規則例を示す図である。

【図１０】専用エディタにより、推論規則に適用条件を
選択する方法を説明する図である。

【図１１】述語論理における適用条件のチェック例を示
す図である。

【図１２】第２実施例を説明する図である。

【図１３】新しい適用条件をテキスト・エディタで作成
する説明図である。

【図１４】新しい適用条件の内容の一部を示す図であ
る。

【図１５】新しい適用条件の作成とチェック例を示す図
である。

【符号の説明】

１ 適用条件記憶部 ２ 適用条件設定部 ３ 証明実行部 ４ 適用条件作成部

Claims (6)

【特許請求の範囲】
1. 【請求項１】 推論規則に適用する適用条件を記憶する
   適用条件記憶部（１）と、推論規則を格納し使用する推
   論規則について前記適用条件記憶部（１）より必要とす
   る適用条件を選択し使用する推論規則とその適用条件の
   組み合せを設定する適用条件設定部（２）と、この使用
   する推論規則を適用して証明を行う際に、この使用する
   推論規則と選択した適用条件の組み合せが満足するもの
   であるか否かの確認を行う証明実行部（３）とを備えた
   ことを特徴とする適用条件処理装置。
2. 【請求項２】 前記証明実行部（３）は、前記推論規則
   と選択した適用条件の組み合せが満足するものであるか
   否かの確認を証明完成後でなければできない場合は、証
   明完成後に確認するようにしたことを特徴とする請求項
   １記載の適用条件処理装置。
3. 【請求項３】 推論規則に適用する適用条件を記憶する
   適用条件記憶部（１）と、推論規則に適用する適用条件
   を作成する適用条件作成部（４）と、推論規則を格納し
   使用する推論規則について前記適用条件記憶部（１）、
   前記適用条件作成部（４）より必要とする適用条件を選
   択して使用する推論規則とその適用条件の組み合せを設
   定する適用条件設定部（２）と、この使用する推論規則
   を適用して証明を行う際に、この使用する推論規則と選
   択した適用条件の組み合せが満足するものであるか否か
   の確認を行う証明実行部（３）とを備えたことを特徴と
   する適用条件処理装置。
4. 【請求項４】 前記証明実行部（３）は、前記推論規則
   と選択した適用条件の組み合せが満足するものであるか
   否かの確認を証明完成後でなければできない場合は、証
   明完成後に確認するようにしたことを特徴とする請求項
   ３記載の適用条件処理装置。
5. 【請求項５】 公理に適用する適用条件を記憶する適用
   条件記憶部（１）と、公理を格納し使用する公理につい
   て前記適用条件記憶部（１）より必要とする適用条件を
   選択し使用する公理とその適用条件の組み合せを設定す
   る適用条件設定部（２）と、この使用する公理を適用し
   て証明を行う際に、この使用する公理と選択した適用条
   件の組み合せが満足するものであるか否かの確認を行う
   証明実行部（３）とを備えたことを特徴とする適用条件
   処理装置。
6. 【請求項６】 公理に適用する適用条件を記憶する適用
   条件記憶部（１）と、公理に適用する適用条件を作成す
   る適用条件作成部（４）と、公理を格納し使用する公理
   について前記適用条件記憶部（１）、前記適用条件作成
   部（４）より必要とする適用条件を選択し使用する公理
   とその適用条件の組み合せを設定する適用条件設定部
   （２）と、この使用する公理を適用して証明を行う際
   に、この使用する公理と選択した適用条件の組み合せが
   満足するものであるか否かの確認を行う証明実行部
   （３）とを備えたことを特徴とする適用条件処理装置。