(57)【要約】【課題】  従来の導出法やタブロー法を用いたものでは、すべての解を導くことは不可能である場合があったが、これを可能とするため、否定を含む等式で解を表現する自動定理証明装置をつくる。【解決手段】  導出法を用いて、（Ａ１）等号以外の述語に導出法を適用して、等号以外の述語を含まない論理式を導く、（Ａ２）等号以外の述語を含まない論理式を、解を表現する標準的な形（等式の標準形）に変形する、あるいは、タブロー法を用いて、（Ｂ１）葉が等号以外の枝が閉じているタブロー木を生成する、（Ｂ２）等号の葉の否定の連言を∃で束縛した論理式を標準形に変形する、また共通に、（３）肯偽でない選言標準形がえられたならばそれを出力し、（４）上記のＡ１、Ａ２（あるいはＢ１、Ｂ２）あるいは、Ａ１（あるいはＢ１）から（３）までの演算あるいは処理を繰り返し行う自動定理証明装置とする。【選択図】  図１０
2005044303.tif 000002
【特許請求の範囲】
【請求項１】
公理あるいは定理の入力データを入力する入力部と、定理が自由変数を持たない（閉論理式）場合は公理から定理を推論可能か否か判定し、定理が自由変数を持つ場合は公理から上記の定理を推論可能になる自由変数の値（解）を論理演算によって導く機能を備えた演算部と、プログラムあるいは、上記の入力データや演算途中のデータ、あるいは演算結果を保存する記憶部と、演算結果を表示する表示部あるいは演算結果を伝送する伝送部とを備えた装置であって、
（１）等号以外の述語に導出法を適用して、等号以外の述語を含まない論理式を導く演算と、
（２）等号以外の述語を含まない論理式を、解を表現する標準的な形（等式の標準形）に変形する演算と、
（３）肯偽でない選言標準形を出力する処理と、
（４）上記の（１）、（２）あるいは（１）から（３）までの演算あるいは処理を繰り返し行うことを特徴とする自動定理証明装置。
【請求項２】
公理あるいは定理の入力データを入力する入力部と、定理が自由変数を持たない（閉論理式）場合は公理から定理を推論可能か否か判定し、定理が自由変数を持つ場合は公理から上記の定理を推論可能になる自由変数の値（解）を論理演算によって導く機能を備えた演算部と、プログラムあるいは、上記の入力データや演算途中のデータ、あるいは演算結果を保存する記憶部と、演算結果を表示する表示部あるいは演算結果を伝送する伝送部とを備えた装置であって、
（１）葉が等号以外の枝は閉じているタブロー木を生成する演算と、
（２）等号の葉の否定の連言を∃で束縛した論理式を標準形に変形する演算と、
（３）肯偽でない選言標準形を出力する処理と、
（４）上記の（１）、（２）あるいは（１）から（３）までの演算あるいは処理を繰り返し行うことを特徴とする自動定理証明装置。
【発明の詳細な説明】
【技術分野】
【０００１】
この発明は、論理式で表される定理を公理から導く自動定理証明装置に関している。
【背景技術】
【０００２】
一般に、自動定理証明装置は、あらかじめ用意した閉論理式の集合（公理と呼ぶ）に対して、論理式（定理）が入力されると、定理が自由変数を持たない（閉論理式）場合は公理から定理を推論可能か否か判定し、定理が自由変数を持つ場合は公理から上記の定理を推論可能になる自由変数の値（解）を導く機能を備えている。
【０００３】
従来の自動定理証明装置では、主に、導出法やタブロー法、あるいはその傍流である線形導出法、パラモジュレーション、節タブロー法、連結タブロー法、あるいは、超タブロー法などが知られおり、すでにそれに関する論文等が複数公表されている。
【０００４】
以下ではこれらの手法の動作を、次の論理式
∀ｘ∀ｙ（（∃ｚ∃ｗ（ｘ＝ｆ（ｚ，ｗ）∧（ｚ≠ａ∨ｗ≠ｂ∨ｚ＝ｗ）→
¬ｐ（ｘ，ｙ））∨¬ｒ（ｙ）∨¬ｓ（ｙ））
∀ｘ∀ｙ（（∃ｚ∃ｗ（ｘ＝ｆ（ｚ，ｗ）∧ｚ≠ｗ∧ｗ＝ｂ）→
¬ｐ（ｘ，ｙ））∨ｒ（ｙ）∨¬ｓ（ｙ））
∀ｙ（ｓ（ｙ）∨ｑ（ｙ））
とクラークの等号公理を公理として用い、
∀ｙ（ｐ（ｘ，ｙ）→ｑ（ｙ））
を定理として用いて説明する。
【０００５】
ここでクラークの等号公理を公理の一部として用いるが、これは次のようなものであり、形式論理学においては、よく知られている。
１）∀ｘ（ｘ＝ｘ）
これは、任意のｘについてｘ＝ｘであるということを表している。
２）∀ｘ∀ｙ（ｘ＝ｙ→ｙ＝ｘ）
これは、任意のｘと任意のｙについて、ｘ＝ｙならば、ｙ＝ｘであることを表している。３）∀ｘ∀ｙ∀ｚ（ｘ＝ｙ∧ｙ＝ｚ→ｘ＝ｚ）
これは、任意のｘ、任意のｙ、任意のｚについて、ｘ＝ｙでありかつｙ＝ｚであるならば、ｘ＝ｚであることを表している。
４）各関数記号ｆについて
∀ｘ１∀ｙ１…∀ｘｎ∀ｙｎ（ｘ１＝ｙ１∧…∧ｘｎ＝ｙｎ→ｆ（ｘ１，…，ｘｎ）＝ｆ（ｙ１，…，ｙｎ））
∀ｘ１∀ｙ１…∀ｘｎ∀ｙｎ（ｆ（ｘ１，…，ｘｎ）＝ｆ（ｙ１，…，ｙｎ）→ｘ１＝ｙ１∧…∧ｘｎ＝ｙｎ）
これらは、関数について、その変数のそれぞれが等しいときは、その関数値もまた等しく、逆に、その関数値が等しいときは、その変数のそれぞれが等しいことを表している。
５）各述語記号ｐについて
∀ｘ１∀ｙ１…∀ｘｎ∀ｙｎ（ｘ１＝ｙ１∧…∧ｘｎ＝ｙｎ→（ｐ（ｘ１，…，ｘｎ）→ｐ（ｙ１，…，ｙｎ）））
これは、述語記号について、その変数の組ｘと組ｙとの２組の値があって、それらがそれぞれ等しいときには、各述語記号ｐが組ｘで成立するときには、各述語記号ｐが組ｙで成立することを表している。
６）異なる関数記号ｆ，ｇについて
∀ｘ１…∀ｘｎ∀ｙ１…∀ｙｍ（ｆ（ｘ１，…，ｘｎ）≠ｇ（ｙ１，…，ｙｍ））
これは、関数記号ｆ，ｇが異なるときには、任意の組ｘと任意の組ｙについてその関数値が異なることを表している。
７）変数ｘが現れるｘ以外の項ｔ［ｘ］のそれぞれについて
∀ｘ（ｔ［ｘ］≠ｘ）
という３つの論理式と５種類の集合である。
上記の項については、一般に次の様に定義される。
７−１）変数は項である。
７−２）定数記号は項である。
７−３）ｆがｎ項の関数記号あるいは演算記号、ｔ１，．．．，ｔｎ、が項であれば、ｆ（ｔ１，．．．，ｔｎ）、も項である。ここで、ｘとｘ以外の項ｔ［ｘ］とは、任意のｘについて、上記の意味で等しくないことを示している。
【０００６】
上記の公理に関する定理の解は「ｆ（ａ，ｂ），ｆ（ｂ，ｂ）以外のｆ（ｚ，ｂ）の形の項」である。これを従来の手法で導こうとすると次のようになる。
【０００７】
まず、公理と、定理の否定を節形式に変形する。ちなみに、原子式または原子式の否定は、リテラルと呼ばれるが、ここで、節形式とは、有限個のリテラルＬ１，．．．，Ｌｋ、を論理和（∨）で結んだ形の論理式、Ｌ１∨…∨Ｌｋ、のことである。その結果は次のようになる。
【０００８】
∀ｘ∀ｙ∀ｚ∀ｗ（¬ｐ（ｘ，ｙ）∨¬ｒ（ｙ）∨¬ｓ（ｙ）∨ｘ≠ｆ（ｚ，ｗ）∨ｚ＝ａ））
∀ｘ∀ｙ∀ｚ∀ｗ（¬ｐ（ｘ，ｙ）∨¬ｒ（ｙ）∨¬ｓ（ｙ）∨ｘ≠ｆ（ｚ，ｗ）∨ｗ＝ｂ））
∀ｘ∀ｙ∀ｚ∀ｗ（¬ｐ（ｘ，ｙ）∨¬ｒ（ｙ）∨¬ｓ（ｙ）∨ｘ≠ｆ（ｚ，ｗ）∨ｚ≠ｗ））
∀ｘ∀ｙ∀ｚ∀ｗ（¬ｐ（ｘ，ｙ）∨ｒ（ｙ）∨¬ｓ（ｙ）∨ｘ≠ｆ（ｚ，ｗ）∨ｚ＝ｗ∨ｗ≠ｂ））
∀ｙ（ｓ（ｙ）∨ｑ（ｙ））
∀ｘ（ｘ＝ｘ）
∀ｘ∀ｙ（ｘ≠ｙ∨ｙ＝ｘ）
∀ｘ∀ｙ∀ｚ（ｘ≠ｙ∨ｙ≠ｚ∨ｘ＝ｚ）
∀ｘ１∀ｙ１…∀ｘｎ∀ｙｎ（ｘ１≠ｙ１∨…∨ｘｎ≠ｙｎ∨ｆ（ｘ１，…，ｘｎ）＝ｆ（ｙ１，…，ｙｎ））  
∀ｘ１∀ｙ１…∀ｘｎ∀ｙｎ（ｆ（ｘ１，…，ｘｎ）≠ｆ（ｙ１，…，ｙｎ）∨ｘ１＝ｙ１∨…∨ｘｎ＝ｙｎ）
∀ｘ１∀ｙ１…∀ｘｎ∀ｙｎ（ｘ１≠ｙ１∨…∨ｘｎ≠ｙｎ∨¬ｐ（ｘ１，…，ｘｎ）∨ｐ（ｙ１，…，ｙｎ））
∀ｘ１…∀ｘｎ∀ｙ１…∀ｙｍ（ｆ（ｘ１，…，ｘｎ）≠ｇ（ｙ１，…，ｙｍ））
∀ｘ（ｔ［ｘ］≠ｘ）
ｐ（ｘ，ｕ（ｘ））
¬ｑ（ｕ（ｘ））
【０００９】
導出法では、図８に示すフローチャートに沿って論理演算を行い、図１のような過程を経て空節を導出する。なお、この図１ではｘは束縛変数であるが、∀による束縛を省略してある。一般に、導出法では、次のどちらかの手続きとなる。
（１）｛Ｌ１，…，Ｌｎ｝、を、Ｌ１∧…∧Ｌｎ、空節｛  ｝をＴ（真）と解釈すれば、導出原理は、選言標準形の論理式の恒真性を判定する手続きとなる。
あるいは
（２）｛Ｌ１，…，Ｌｎ｝、を、Ｌ１∨…∨Ｌｎ、空節｛  ｝をＦ（偽）と解釈すれば、
導出原理は連言標準形の論理式の充足不可能性を判定する手続きとなる。
つまり、空節とは、恒真の論理式か充足不可能な論理式であるが、図１の場合は、充足不可能な論理式である。
【００１０】
この過程で導かれた解は、２つの代入｛ｆ（ｚ１，ｂ）／ｘ｝と｛ｃ／ｚ１｝を合成した代入｛ｆ（ｃ，ｂ）／ｘ｝で表現される。ここで、代入とは、ｓが項のとき、ｓ｛ａ１／ｘ１，…，ａｎ／ｘｎ｝で、ｓに現れる変数ｘｉを項ａｉで置き換えた項を示す。上記の代入では「ｆ（ａ，ｂ），ｆ（ｂ，ｂ）以外のｆ（ｚ，ｂ）の形の項」のうちの１つｆ（ｃ，ｂ）が解であることを表現しており、残りの解を導くためにはｘに関する別の代入を求める作業を繰り返し行わなければならない。
【００１１】
また、タブロー法では、図９に示すフローチャートに沿って、論理演算を行うが、図２のような閉じたタブロー木をつくる。ここで、タブロー木が閉じているとは、各々の枝の中にその枝の葉（木の末端の原子式）の否定の原子式が含まれている状態のことである。このタブロー木から導かれる解は２つの代入｛ｆ（ｚ２，ｗ２）／ｘ｝と｛ｃ／ｚ２，ｂ／ｗ２｝を合成した代入｛ｆ（ｃ，ｂ）／ｘ｝で表現されている。残りの解を導くためには、導出法と同様に、ｘに関する別の代入を求めなければならない。しかし「ｆ（ａ，ｂ），ｆ（ｂ，ｂ）以外のｆ（ｚ，ｂ）の形の項」という解は無数にあるので、導出法やタブロー法ではすべての解を導くことは不可能である。
【００１２】
以上のように、従来の方法では、自由変数への代入で解を表現するので、解が「ａ以外」というような場合にａ以外の解を列挙しなければならないという問題がある。
【００１３】
次に、従来の方法をより詳しく説明する。以下では、クラークの等号公理をＥ（Σ）で表し、論理式φと同じ自由変数を持ち、Ｅ（Σ）の下で同値な選言標準形（ＤＮＦ）を、記号ＤＮＦ（φ）で表す。また、関係φ∠ＭＴψを、任意の変数割り当てＶに対してＭ〔φ〕Ｖ＝ＴならばＭ〔ψ〕Ｖ＝Ｔが成り立つことと定義し、関係φ∠ＭＦψを、任意の変数割り当てＶに対してＭ〔φ〕Ｖ＝ＦならばＭ〔ψ〕Ｖ＝Ｆが成り立つことと定義する。さらに、以下では、次の補題を用いる。
【００１４】
［補題１］
Ｆ＋、Ｆ−、Ｇ＋、Ｇ−を論理式、△を閉論理式の集合とする任意の述語の置換Ωに対して、
Ｆ＋Ω∠ΔＴＧ＋Ω  かつ  Ｆ−Ω∠ΔＦＧ−Ω
が成り立つと仮定する。このとき、任意の論理式φと任意のｎ≧０について、次の２式が成り立つ。
φ｛Ｆ＋／ｐ；Ｆ−／ｐ｜ｘ｝ｎ｛ｕ／ｐ｝
∠ΔＴφ｛Ｇ＋／ｐ；Ｇ−／ｐ｜ｘ｝ｎ｛ｕ／ｐ｝
φ｛Ｆ−／ｐ；Ｆ＋／ｐ｜ｘ｝ｎ｛ｕ／ｐ｝
∠ΔＦφ｛Ｇ−／ｐ；Ｇ＋／ｐ｜ｘ｝ｎ｛ｕ／ｐ｝
【００１５】
［補題２］
φを閉論理式とする。次の式が成り立つ。
Ｅ（Σ）｜＝３φ｛ｕ／ｐ｝  ⇔ＤＮＦ（φ｛Ｆ／ｐ；Ｔ／ｐ｝）＝Ｔ
【００１６】
また、以下では、次の手続きを手続きの骨格Ｓと呼ぶことにし、入力Ｇをゴールと呼ぶ。
手続きの骨格Ｓ：
入力：論理式Ｇ、
内部バラメータ：述語の置換Θ
１．ｎ＝０とおく．
２．    ２．１から２．５を繰り返す。
２．１．Ｇｎ＝ＧΘｎ、ＤＮＦｎ＝ＤＮＦ（ＧΘｎ｛Ｆ／ｐ；Ｔ／ｐ｝）を計算する。
２．２・ＤＮＦｎ≠Ｔ、≠Ｆの場合、Ｔを表示して手続きを終了する。
２．３  ＤＮＦｎ≠Ｔ、≠Ｆ．すなわちＤＮＦｎが自由変数を含む場合、ＤＮＦｎを表示する。
２．４．Ｇｎがｐを含まない場合、手続きを終了する。
２．５    Ｇｎがｐを含む場合、ｎを１つ増やして、
２．１へ戻る。
【００１７】
この手続きに関して重要な点は、任意のＧ、Θ、ｎに対して選言標準形ＤＮＦ（ＧΘｎ｛Ｆ／ｐ；Ｔ／ｐ｝）を有限時間で計算できるアルゴリズムが存在することである。つまり、この手続きはｎが一定の値のまま２．１のところで動き続けることはなくｎを増やしながら動き続けるか、２．２または２．４で終了する。
【００１８】
これまでに提案された手続きに、
Θ＝｛Ｐ＋∧¬Ｐ−／ｐ；Ｐ＋∨¬Ｐ−／ｐ｜ｘ｝
とおき、手続きの骨格Ｓを実行するものがある。上記の縦線、｜、の右側に記載されたものは変数である。以下では、これを手続きＰと呼ぶことにする。また、この手続きに適用できる論理プログラムのクラスをＦＬＰと呼ぶ。
【００１９】
［定義１］
次の形の論理式
∀ｘ（ｐ（ｘ）←Ｐ＋）        （１）
∀ｘ（¬ｐ（ｘ）←Ｐ＋）      （２）
とＥ（Σ）からなる論理式の集合をＦＬＰと呼ぶ、但し．ベクトルｐに現れる述語記号ｐｉは等号以外であり、すべて互いに異なるものと仮定する。また、Ｐ＋とＰ−は、３値論理での同値関係、⇔、が現れない論理式のベクトルであり、Ｐｉ＋とＰｉ−、現れる自由変数は、Ｐｉ（ｘ）（＝Ｐｉ（ｘｉ、‥‥ｘｍｉ））にも現れると板定する。式（１）の形の論理式を、正の述語定義、式（２）の形の論理式を、負の述語定義と呼ぶ。
【００２０】
〔例１〕
次の４つの論理式
∀ｘ（ｐ１（ｘ）←ｘ＝ａ）、
∀ｘ（¬ｐ１（ｘ）←¬ｐ２（ｘ））、
∀ｘ（ｐ２（ｘ）←Ｆ）、
∀ｘ（¬ｐ２（ｘ）←∃ｙ（ｘ＝ｆ（ｙ）））、
とＥ（Σ）からなる論理式の集合はＦＬＰである。また、上から順に、
ｐ１の正の述語定義、
ｐ１の負の述語定義、
Ｐ２の正の述語定義、
Ｐ２の負の述語定義、である。
【００２１】
ここで、非論理的公理系Ｔも含めた公理系から論理式ψが導出されることを  
Ｔ  ｜−  ψ  、と表し、｜−  ψ  という演繹において、推論規則が妥当、かつ前提がすべて恒真式であれば、帰結ψも恒真式である。特に、推論規則が妥当で公理系がすべて恒真式であれば、そこから導かれる定理もすべて恒真式である。つまり、
｜−  ψ  ならば  ｜＝  ψ  。
３値論理についての論理的帰結である場合を、｜＝３、で示す。また、同様に、３値論理
について真理値が等しいという意味での同値関係にある場合を、≡３、で示す。
【００２２】
このとき、手続きＰを導入したことによって、次の定理が簡潔に表現できる。
〔定理１〕
Θ＝｛Ｐ＋∧¬Ｐ−／ｐ；Ｐ＋∨¬Ｐ−／ｐ｜ｘ｝
Ｐ＝｛Ｐ＋∨ｐ（ｘ）｝∧（¬Ｐ−∨¬ｐ（ｘ））
∧（Ｐ＋∨¬Ｐ−）
Ｐｕ＝（（Ｐ＋∧¬Ｐ−）∨ｕ）∧（Ｐ＋∧¬Ｐ−）
とおく。また、Ｇを任意の閉論理式とする。このとき、次の３つ
Ｅ（Σ）、∀ｘ（ｐ（ｘ）⇔Ｐ）｜＝３Ｇ
Ｅ（Σ）、∀ｘ（ｐ（ｘ）⇔Ｐｕ）｜＝３Ｇ
∃ｎ  ｓ．ｔ．  Ｅ（Σ）｜＝３ＧΘｎ｛ｕ／ｐ｝
は同値であり、この３つが成り立つならば、
Ｅ（Σ）、∀ｘ（ｐ（ｘ）←Ｐ＋）、∀ｘ（¬ｐ（ｘ）←Ｐ−）｜＝Ｇ
が成り立つ。
【００２３】
［定義２］
完備プログラム
Ｅ（Σ）∪｛∀ｘ（ｐ（ｘ）⇔Ｐ）｝
をＦＬＰ  Ｅ（Σ〉∪｛∀ｘ（ｐ（ｘ）←Ｐ＋）、∀ｘ（¬ｐ（ｘ）←Ｐ−）｝
の完備化と呼ぶ。
【００２４】
ＦＬＰの完備化は、ＦＬＰと、２値論理で同値な完備プログラムである。また、定理１より、手続きＰはＦＬＰの完備化の３値論理の論理的帰結しか判定できないことがわかる。
【００２５】
〔例２〕
Ｅ（Σ）と
∀ｘ（ｐ１（ｘ）←ｘ＝ａ）、
∀ｘ（¬ｐ１（ｘ）←¬ｐ２（ｘ））
∀ｘ（ｐ２（ｘ）←¬ｐ１（ｘ））、
∀ｘ（¬ｐ２（ｘ）←ｐ１（ｘ））、
からなるＦＬＰをΠ２とおく、Π２｜＝ｐ１（ａ）である。
定理１の∀ｘ（ｐ（ｘ）⇔Ｐｕ）にあたる述語定義は
∀ｘ（ｐ１（ｘ）⇔
（（ｘ＝ａ∧¬ｐ２（ｘ））Ｖｕ∧（ｘ＝ａ∨¬ｐ２（ｘ）））、
∀ｘ（ｐ２（ｘ）⇔¬ｐ１（ｘ））、
と３値論理で同値であるｐ１（ａ）とｐ２（ａ）にｕを割り当てる解釈はこれらの３値論理のモデルなので、
ｐ１（ａ）はＥ（Σ）∪∀ｘ（ｐ（ｘ）⇔Ｐｕ）
の３値論理の論理的帰結ではない。したがって、定理１より手続きＰは、
Π２｜＝ｐ１（ａ）
であることを判定できないことがわかる。
【００２６】
実際に手続きＰを実行してみると．
Ｇ０＝ｐ１（ａ）
Ｇ０ＦＴ＝ＤＮＦ０＝Ｆ
Ｇ１＝ａ＝ａ∧¬ｐ２（ａ）
Ｇ１ＦＴ＝ａ＝ａ∧¬ｐ２（ａ）
ＤＮＦＴ＝Ｆ
となり、すべてのｎでＤＮＦ１＝Ｆとなる。
【非特許文献１】秋葉  澄孝、佐藤  泰介、元吉  文男：論理プログラムの新しい完備化と展開に基づく計算手続きについて、情報処理学会論文誌、Vol.41，No、11，ｐｐ.3023−3036（2000）
【非特許文献２】Kunen, K.; Negation in Logic Programming, J. LogicProgramming, Vo1. 4, No. 4, pp. 289-308 (1987)
【発明の開示】
【発明が解決しようとする課題】
【００２７】
従来の導出法やタブロー法を用いたものでは、すべての解を導くことは不可能である場合があったが、これを可能とする、否定を含む等式で解を表現する自動定理証明装置をつくることである。
【課題を解決するための手段】
【００２８】
この発明は、等号以外の述語に従来の定理証明手法を適用し、等号以外の述語を含まない論理式を、解を表現する適切な形に変形するものである。従来の手法のうち導出法を用いるものは、空節を導出する。この場合の空節とは充足不能な論理式のことである。したがって、導出法によって等号以外の述語を含まない論理式が導かれたならば、その論理式が充足不能になるような自由変数の値は定理の解になる。別な言い方をすると、その論理式の否定が恒真になるような自由変数の値は定理の解になる。
【００２９】
この原理に基づき、本発明の自動定理証明装置では、
（Ａ１）等号以外の述語に導出法を適用して、等号以外の述語を含まない論理式を導く、（Ａ２）等号以外の述語を含まない論理式を、解を表現する標準的な形（等式の標準形）に変形する、
という論理演算をおこなうという特徴を備えている。
【００３０】
あるいは、タブロー法を用いて、
（Ｂ１）葉が等号以外の枝が閉じているタブロー木を生成する、
（Ｂ２）等号の葉の否定の連言を∃で束縛した論理式を標準形に変形する、という論理演算をおこなうという特徴を備えている。
【発明の効果】
【００３１】
従来の導出法やタブロー法ではすべての解を導くことは不可能である場合があったが、本発明では、このような場合に、否定を含む等式で解を表現する自動定理証明装置をつくることができる。
【発明を実施するための最良の形態】
【００３２】
本発明の自動定理証明装置は、図７に示すように、閉論理式の集合（つまり公理）や論理式（つまり定理）などの入力データを入力する入力部１と、公理から定理が自由変数を持たない（閉論理式）場合は公理から定理を推論可能か否か判定し、定理が自由変数を持つ場合は公理から上記の定理を推論可能になる自由変数の値（解）を論理演算によって導く機能を備えた演算部２と、プログラムや上記の入力データや演算途中のデータ、あるいは演算結果を保存する記憶部３と、演算結果を表示する表示部４あるいは演算結果を伝送する伝送部５とを備えた装置であって、その演算手順に特徴があり、これを以下に説明する。
【実施例１】
【００３３】
上記の自動定理証明装置において、演算手順を従来の手法の説明で用いた例に適用して説明する。以下に示す本発明の自動定理証明装置では、図１０に示すフローチャートに沿
って論理演算を行う。図１０のＦ１において、導出法で新しい論理式の導出を試みる計算機プログラムについては、既によく知られており、ここでもそれを用いることができる。また、Ｆ２において、論理式を選言標準形に変形するが、この変形については、いかなる論理式も選言標準形に変形に変形することが可能であることは既に証明されている。その演算においては、
（１）等号以外の述語に導出法を適用して、等号以外の述語を含まない論理式を導く、
（２）等号以外の述語を含まない論理式を、解を表現する標準的な形（等式の標準形）に変形する、
という特徴がある。
（３）また、肯偽でない選言標準形が得られたならばそれを出力し、
（４）上記の（１）、（２）あるいは（１）から（３）までの演算あるいは処理を繰り返し行うという特徴がある。
【００３４】
まず、導出法を図１の途中まで適用すると、図３に示すように、等号以外の述語を含まない論理式、
∀ｚ１∀ｗ１（ｘ≠ｆ（ｚ１、ｗ１）∨ｚ１＝ａ∨ｚ１＝ｗ１∨ｗ１≠ｂ）
が得られる。これの否定をとってから選言標準形に変形すると、
¬∀ｚ１∀ｗ１（ｘ≠ｆ（ｚ１，ｗ１）∨ｚ１＝ａ∨ｚ１＝ｗ１∨ｗ１≠ｂ）≡∃ｚ１∃ｗ１（ｘ＝ｆ（ｚ１，ｗ１）∧ｚ１≠ａ∧ｚ１≠ｗ１∧ｗ１＝ｂ）
≡∃ｚ（ｘ＝ｆ（ｚ，ｂ））∧ｘ≠ｆ（ａ，ｂ）∧ｘ≠ｆ（ｂ，ｂ）
となる最後の式は「ｆ（ａ，ｂ），ｆ（ｂ，ｂ）以外のｆ（ｚ，ｂ）の形の項」という解を表現している。
【００３５】
導出法の適用のしかたによっては、図４に示すように、等号以外の述語を含まない論理式に定理の自由変数が含まれない場合がある。このようなときには、導出法を適用したときに使用した代入を等式で表し、その否定の選言を論理式に付け加える。図４では一番下の論理式には定理の自由変数ｘが含まれていない。そこで、代入｛ｘ１／ｘ｝を等式ｘ１＝ｘと表し、これの否定を論理式に付け加えて、
∀ｘ１∀ｚ１∀ｗ１（ｘ１≠ｆ（ｚ１，ｗ１）∨ｚ１＝ａ∨ｚ１＝ｗ１∨ｗ１≠ｂ∨ｘ１≠ｘ）、
をつくる。これの否定をとってから選言標準形に変形すると、
¬∀ｘ１∀ｚ１∀ｗ１（ｘ１≠ｆ（ｚ１，ｗ１）∨ｚ１＝ａ∨ｚ１＝ｗ１∨ｗ１≠ｂ∨ｘ１≠ｘ）、
≡∃ｘ１∃ｚ１∃ｗ１（ｘ１＝ｆ（ｚ１，ｗ１）∧ｚ１≠ａ∧ｚ１≠ｗ１∧ｗ１＝ｂ∧ｘ１＝ｘ）
≡∃ｚ（ｘ＝ｆ（ｚ，ｂ））∧ｘ≠ｆ（ａ，ｂ）∧ｘ≠ｆ（ｂ，ｂ）、
となり、図３のときと同じ解の表現が得られる。この過程は解および等号以外の述語を含まない論理式と無関係な代入は使用する必要はない。図４では｛ｕ（ｘ１）／ｙ１｝という代入は使用する必要はない。しかし、使用しても計算量が増えるだけで正しい解が得られる。
【００３６】
上の例で、この代入も等式で表して、その否定を付け加えると
∀ｘ１∀ｚ１∀ｗ１∀ｙ１（ｘ１≠ｆ（ｚ１，ｗ１）∨ｚ１＝ａ∨ｚ１＝ｗ１∨ｗ１≠ｂ∨ｘ１≠ｘ∨ｕ（ｘ）≠ｙ１）
になり、これの否定をとってから選言標準形に変形すると、
¬∀ｘ１∀ｚ１∀ｗ１∀ｙ１（ｘ１≠ｆ（ｚ１，ｗ１）∨ｚ１＝ａ∨ｚ１＝ｗ１∨ｗ１≠ｂ∨ｘ１≠ｘ∨ｕ（ｘ）≠ｙ１）
≡∃ｘ１∃ｚ１∃ｗ１∃ｙ１（ｘ１＝ｆ（ｚ１，ｗ１）∧ｚ１≠ａ∧ｚ１≠ｗ１∧ｗ１＝ｂ∧ｘ１＝ｘ∧ｕ（ｘ）＝ｙ１）
≡∃ｚ（ｘ＝ｆ（ｚ，ｂ））∧ｘ≠ｆ（ａ，ｂ）∧ｘ≠ｆ（ｂ，ｂ）
となり同じ結果が得られる。
【００３７】
次に、タブロー法を用いる例を示す。タブロー法は閉じたタブロー木を生成するが、閉じたタブロー木の枝は、枝の上のすべてのリテラルを充足するモデルが存在しないことを表し、閉じたタブロー木全体は、どの枝も充足不能なことを表している。したがって、葉が等号以外の枝が閉じているタブロー木を生成すると、すべての葉が充足不能になるような自由変数の値は定理の解になる。つまり、葉の否定の連言が恒真になるような自由変数の値は定理の解になる。
【００３８】
この原理に基づく新しい手法として、（１）葉が等号以外の枝が閉じているタブロー木を生成する、（２）等号の葉の否定の連言を∃で束縛した論理式を標準形に変形する、という方法が考えられる。（３）この場合もまた、肯偽でない選言標準形がえられたならばそれを出力し、（４）上記の（１）、（２）あるいは（１）から（３）までの演算あるいは処理を繰り返し行うものである。
この場合のフローチャートを図１１に示す。図１１のＧ１において、新しいタブロー木の生成を行うための計算機プログラムは、既によく知られており、ここでもそれを用いることができる。また、Ｇ２において、選言標準形に変形するが、上記の導出法を用いる場合と同様に、いかなる論理式も選言標準形に変形することができる。
【００３９】
この方法を従来の手法の説明で用いた例に適用してみる。葉が等号以外枝が閉じているタブロー木は、図５のように生成される。この木の等号の葉は、
ｘ１≠ｆ（ｚ１，ｗ１）、ｚ１＝ａ、ｘ２≠ｆ（ｚ２，ｗ２）、ｚ２＝ｗ２、ｗ２≠ｂ、に代入、
｛ｘ／ｘ１，ｕ（ｘ）／ｙ１｝、｛ｘ／ｘ２，ｕ（ｘ）／ｙ２｝、
を適用したものである。等号の葉の否定の連言を∃で束縛した論理式は、
∃ｚ１∃ｗ１∃ｚ２∃ｗ２（ｘ＝ｆ（ｚ１，ｗ１）∧ｚ１≠ａ∧ｘ＝ｆ（ｚ２，ｗ２）∧ｚ２≠ｗ２∧ｗ２＝ｂ）、
なので、これを選言標準形に変形すると、
∃ｚ１∃ｗ１∃ｚ２∃ｗ２（ｘ＝ｆ（ｚ１，ｗ１）∧ｚ１≠ａ∧ｘ＝ｆ（ｚ２，ｗ２）∧ｚ２≠ｗ２∧ｗ２＝ｂ）、
≡∃ｚ（ｘ＝ｆ（ｚ，ｂ）∧ｚ≠ａ∧ｚ≠ｂ）、
≡∃ｚ（ｘ＝ｆ（ｚ，ｂ））∧ｘ≠ｆ（ａ，ｂ）∧ｘ≠ｆ（ｂ，ｂ）、
となり、解を表現する等式が得られる。
【００４０】
タブロー法を用いる場合でも、図６に示すように、タブロー木の作り方によっては、葉に定理の自由変数が含まれないことがある。そのときには、タブロー木をつくったときの代入を等式で表し、その連言を論理式に付け加えればよい。図６のタブロー木から等号の葉の否定の連言を∃で束縛した論理式をつくると、
∃ｘ１∃ｚ１∃ｗ１∃ｚ２∃ｗ２（ｘ１＝ｆ（ｚ１，ｗ１）∧ｚ１≠ａ∧ｘ＝ｆ（ｚ２，ｗ２）∧ｚ２≠ｗ２∧ｗ２＝ｂ）、
となり、定理の自由変数ｘが含まれない。この論理式とｘに関係がある代入は｛ｘ１／ｘ｝なので、これを表す等式を付け加えてから選言標準形に変形すると、
∃ｘ１∃ｚ１∃ｗ１∃ｚ２∃ｗ２（ｘ１＝ｆ（ｚ１，ｗ１）∧ｚ１≠ａ∧ｘ＝ｆ（ｚ２，ｗ２）∧ｚ２≠ｗ２∧ｗ２＝ｂ∧ｘ１＝ｘ）
≡∃ｚ（ｘ＝ｆ（ｚ，ｂ）∧ｚ≠ａ∧ｚ≠ｂ）
≡∃ｚ（ｘ＝ｆ（ｚ，ｂ））∧ｘ≠ｆ（ａ，ｂ）∧ｘ≠ｆ（ｂ，ｂ）、
となり、図５の場合と同じ等式が得られる。
【００４１】
また、無関係な代入を使用しても正しい解が得られることは、導出法の場合と同様である。例えば、図６で｛ｕ（ｘ１）／ｚ３｝と｛ｕ（ｘ１）／ｚ６｝も使用すると、
∃ｘ１∃ｚ１∃ｗ１∃ｚ２∃ｗ２∃ｚ３∃ｚ６（ｘ１＝ｆ（ｚ１，ｗ１）∧ｚ１≠ａ∧ｘ＝ｆ（ｚ２，ｗ２）∧ｚ２≠ｗ２∧ｗ２＝ｂ∧ｘ１＝ｘ∧ｕ（ｘ１）＝ｚ３∧ｕ（ｘ１）＝ｚ６）
≡∃ｚ（ｘ＝ｆ（ｚ，ｂ）∧ｚ≠ａ∧ｚ≠ｂ）
≡∃ｚ（ｘ＝ｆ（ｚ，ｂ））∧ｘ≠ｆ（ａ，ｂ）∧ｘ≠ｆ（ｂ，ｂ）、
となる。
【００４２】
以上のように、従来の手法を用いて等号以外の述語を含まない論理式を導き、その論理式を適切な形に変形する手法によって、否定を含む等式で解を表現する自動定理証明装置をつくることができる。
【００４３】
以上の例では、等号に関する公理としてクラークの等号公理を用い、解を表現する式の形として選言標準形を用いた。その理由は、等号のみを含む論理式をクラークの等号公理のもとで同値な選言標準形に変形するアルゴリズムが存在するからである。例えば、クラークの等号公理以外の自然数の公理、実数の公理、複素数の公理などでも、その公理に合った標準形とアルゴリズムがあれば、それらを用いることによって、同様の自動定理証明装置をつくることができる。
【実施例２】
【００４４】
上記の自動定理証明装置において、演算手順を従来の手法の説明で用いた例に適用して説明する。
【００４５】
新しい計算手続き、Ｑｉ＋とＱｉ−を次の（Ａ）、（Ｂ）どちらかで定義する。
（Ａ）Ｑｉ＋＝Ｐｉ＋、  Ｑｉ−＝Ｐｉ−∧¬Ｐｉ＋
（Ｂ）Ｑｉ＋＝Ｐｉ＋∧¬Ｐｉ＋、Ｑｉ−＝Ｐｉ−
以下では、Θ＝｛Ｑ＋／ｐ；¬Ｑ−／ｐ｜ｘ｝とおき手続きの骨格Ｓを実行する手続きを、手続きＱと呼ぶ。
【００４６】
このΘよりもΘ＊＝｛Ｐ＋／ｐ；¬Ｐ−／ｐ｜ｘ｝を用いた方が、論理式の置換方法として自然である。しかも、Θ＊を用いた場合の健全性は、付録の補題４を用いて証明でき、手続きＰのΘや上のΘを用いた場合よりも多くの論値的帰結を計算できることは．後述の命題１と同様に証明できる。しかし、完全性を表す定理１のような命題を明らかにするのは、難しい問題である。
【００４７】
ここで、Θ＊を用いた手続きの完全性などの理輸的な研究の準備として、正負の述語を置き換る論理式のうちの一方にΘ＊と同じものを用い、他方に手続きｐと同じものを用いたΘについて調べた結果、このΘを用いた手続き、つまり手挽きＱの能力は次のようになっていることがわかる。
【００４８】
〔定理２〕
Ｑ、Ｑｕ、Θを次のように置く。
Ｑ＝（Ｑ＋∨ｐ（ｘ））∧¬Ｑ−
Ｑｕ＝（Ｑ＋∨ｕ）∧¬Ｑ−
Θ＝｛Ｑ＋／ｐ；¬Ｑ−／ｐ｜ｘ｝
Ｇを任意の閉論理式とする。次の３つは同値である。
Ｅ（Σ）、∀ｘ（ｐ（ｘ）⇔Ｑ）｜＝３Ｇ
Ｅ（Σ）、∀ｘ（ｐ（ｘ）⇔Ｑｕ）｜＝３Ｇ
∃ｎ  ｓ．ｔ．  Ｅ（Σ）｜＝３Ｇ｛ｕ／ｐ｝
また．これらが成り立つならば
Ｅ（Σ）、∀ｘ（ｐ（ｘ）←Ｐ＋）、∀ｘ（¬ｐ（ｘ）←Ｐ）｜＝Ｇ
が成り立つ。
【００４９】
この定理と補題２より、手続きＱはＦＬＰの２値論理での論理的帰結を健全に判定できることと、ＦＬＰの完備化とは異なる完備プログラムであるＥ（Σ）∪∀ｘ（ｐ（ｘ）⇔Ｑ）や、Ｅ（Σ）∪∀ｘ（ｐ（ｘ）⇔Ｑｕ）の３値論理での論理的帰結を健全かつ完全に判定できることがわかる。ここで、健全に判定できるとは、「判定できることは正しい」ということであり、完全に判定できるとは、「正しいことは判定できる」ということを示している。
【００５０】
閉論理式Ｇに対する手続きＱの動作を分類すると、（１）ＧがゴールのときＴを表示する（２）¬Ｇがゴールのとき、Ｔを表示する（３）Ｇ、¬ＧのどちらがゴールでもＴを表示しない、の３つの場合がある。直感的には、これが３値論理が現れる必然性であると考えられる。
【００５１】
完備プログラムの理論を用いると、より詳しく次のように説明できる。Ｅ（Σ）のモデルを任意にとり．それを非特許文献２の方法で拡張した解釈をＭとすると、ＭはＥ（Σ）∪｛∀ｘｐ（ｘ）⇔Ｑ｝）の３値モデルになる。しかも、Ｍが割り当てるＧの真理値にはＴ、Ｆ、ｕの３つの場合があるが、それぞれが手続きＱの動作を分類した上記の３つの場合に対応する手続きＱは、このような手続き的意味を持っている手続きＰと同様に手続きＱも、ゴールが自由変数を含む場合には、ゴールがＦＬＰの論理的帰結となるような解を、否定を含む等式で表現できる。
【００５２】
（例３）Ｇ＝（¬∃ｙ（ｘ＝ｆ（ｆ（ｙ）））∨ｐ１（ｘ））∧¬ｐ２（ｘ）、例１のＦＬＰをΠ１とおき、Π１｜＝Ｇとなるｘを手続きＱで計算する。
Ｑ１＋とＱ１−を前節（Ａ）の仕方で、Ｑ２＋とＱ２−を〈Ｂ〉
の仕方で決めて、
Ｑ１＋＝ｘ＝ａ、    Ｑ１−＝¬Ｐ２〈ｘ〉∧¬ｘ＝ａ
Ｑ２＋＝ｆ∧¬∃ｙ（ｘ＝ｆ〈ｙ〉）、Ｑ２−＝∃ｙ（ｘ＝ｆ（ｙ））
とおく。手続きＱで用いるΘは、
｛ｘ＝ａ／ｐ１，ｆ∧¬∃ｙ（ｘ＝ｆ（ｙ））／ｐ２；
¬（¬ｐ２（ｘ）∧¬ｘ＝ａ）／ｐ１，¬∃ｙ（ｘ＝ｆ（ｙ））／ｐ２｜ｘ｝
である。手続きＱを実行すると、
Ｇ０＝（¬∃ｙ（ｘ＝ｆ（ｆ（ｙ）））∨ｐ１（ｘ））∧¬ｐ２（ｘ）
Ｇ０ＦＴ＝（¬∃ｙ（Ｘ＝ｆ（ｆ（ｙ）））∨ｆ）∧¬Ｔ
ＤＮＦ０＝Ｆ
Ｇ１＝（¬（¬∃ｙ（ｘ＝ｆ（ｆ（ｙ）））∨ｘ＝ａ）∧¬¬∃ｙ（ｘ＝ｆ（ｙ））
Ｇ１ＦＴ＝（¬∃ｙ（ｘ＝ｆ（ｆ（ｙ）））∨ｘ＝ａ）∧¬¬∃ｙ（ｘ＝ｆ（ｙ））
ＤＮＦ１＝∃ｙ（ｘ＝ｆ（ｙ））∧¬∃ｙ（ｘ＝ｆ（ｆ（ｙ）））
となり、これにより、
∃ｙ（ｘ＝ｆ（ｙ））∧¬∃ｙ（ｘ＝ｆ（ｆ（ｙ）））と
いう形の項はΠ１｜＝Ｇの解であることがわかる。例えば、ｘ＝ｆ（ａ）は解であるが、ｘ＝ｆ（ｆ（ａ））はそうとはいえない。
【００５３】
次に、手続きＱと手続きＰを比較する。
〈命題１〉
Θｐ＝（Ｐ＋∧¬Ｐ−／ｐ；Ｐ＋∨¬Ｐ−／ｐ｜ｘ）
Θ＝（Ｑ＋／ｐ；¬Ｑ−／ｐ｜ｘ）
とおく、
Ｅ（Σ）｜＝３ＧΘｐｎ｛ｕ／ｐ｝⇒Ｅ（Σ）｜＝３ＧΘｎ｛ｕ／ｐ｝
が成り立つ。この命題と補題２より、手続きＰがＴを表示するときは手続きＱも必ずＴを
表示することがわかる。
【００５４】
さらに．そのときのｎの値、つまり手続きがゴールを展開した回数に関して、手続きＱの回数は手続きＰの回数以下であることがわかる。また、アトムを置き換える論理式を比較するとΘの論理式はΘｐの論理式の部分論理式なので、展開を１回行う計算量は、手続きＱの方が少ない。すなわち、展開の回数と計算量の両方に関して、手続きＱの方が手続きＰよりも計算の効率が良い。なお、Ｇｎにｐが含まれなくなるまでの手続きＱの展開回数も、手続きＰの展開回数以下である。
【００５５】
また．次の例のように、ＦＬＰの２値論理の論理的帰結の中には、手続きＱでは判定できるが、手続きＰでは判定できないものが存在する。すなわち、手続きＱは手続きＰよりもＦＬＰの論理的帰結を多く判定できる。
【００５６】
〔例４〕
Π２を例２のＦＬＰとする。例２で確かめたとおり、手続きＰではΠ２｜＝ｐ１（ａ）であることを判定できない。しかし、手続きＱでは次のように判定できる。Ｑ１＋、Ｑ１−．Ｑ２＋、Ｑ２−を前節（Ａ）の仕方で決めて、
Ｑ１＋＝ｘ＝ａ、  Ｑ１−＝ｐ２（ｘ）∧¬ｘ＝ａ
Ｑ２＋＝¬ｐ１（ｘ）、  Ｑ２−＝Ｐ１（ｘ）∧¬¬ｐ１（ｘ）
とおく。
【００５７】
任意の述語の置換Ωに対して（¬Ｑ２−）Ω≡３（¬ｐ１（ｘ））Ω
が成り立つので、補題１より手続きＱでは述語の置換
｛ｘ＝ａ／ｐ１，¬Ｐ１（ｘ）／ｐ２；
¬（ｐ２（ｘ）∧¬ｘ＝ａ）／ｐ１，¬ｐ１（ｘ）／ｐ２｜ｘ｝
をΘとして用いても良い。このΘを用いて手続きＱを実行すると
Ｇ０＝ｐ１（ａ）
Ｇ０ＦＴ＝ＤＮＦ０＝Ｆ
Ｇ１＝Ｇ１ＦＴ＝ａ
ＤＮＦ１＝Ｔ
となり、Π２  ｜＝  ｐ１（ａ）、であることがわかる。
【００５８】
（例５）
例４では、Ｑ１＋とＱ１−を前節（Ａ）の仕方で
決めたが．これらを（Ｂ）の仕方で決めて、
Ｑ１＋＝ｘ＝ａ∧¬ｐ２（ｘ）、Ｑ１−＝ｐ２（ｘ）
Ｑ１＋＝¬ｐ１（ｘ）、    Ｑ２＋＝ｐ１（ｘ）∧¬¬ｐ１（ｘ）
とおくと、Π２｜＝ｐ１（ａ）を判定できなくなる。
このことは定理２を用いて次のように説明できる。
【００５９】
定理２の∀ｘ（ｐ（ｘ）⇔Ｑｕ）に相当する述語定義は、
∀ｘ（ｐ１（ｘ）⇔（（ｘ＝ａ∧¬ｐ２（ｘ））∨ｕ）∧¬ｐ２（ｘ）
∀ｘ（ｐ２（ｘ）⇔¬ｐ１（ｘ））
と３値論理で同値であるｐ１（ａ）とｐ２（ａ）にｕを割り当てる解釈はこれらのモデルなので、Ｅ（Σ）、∀ｘ（ｐ（ｘ）⇔Ｑｕ）｜≠３ｐ１（ａ）である。したがって、定理２より手続きＱはΠ２｜＝ｐ１（ａ）であることを判定できないことがわかる。
【００６０】
一方、例４のようにＱ１＋とＱ１−を前節（Ａ）の仕方で決めた場合には、定理２の∀ｘ（ｐ（ｘ）⇔Ｑｕ）に相当する述語定義は、
∀ｘ（ｐ１（ｘ）⇔（ｘ＝ａ∨ｕ）∧（ｘ＝ａ∨¬ｐ２（ｘ））
∀ｘ（ｐ２（ｘ）⇔¬ｐ１（ｘ））
と３値論理で同値である。これらのモデルはｐ１（ａ）にＴを、ｐ２（ａ）にＦを割り当てる解釈であり、Ｐ１（ａ）にｕを割り当てる解釈はモデルではない。したがって、Ｅ（Σ）、∀ｘ（ｐ（ｘ）⇔Ｑｕ）｜＝３Ｐ１（ａ）なので、例４では手続きＱでΠ２｜＝ｐ１（ａ）を判定できた。
【００６１】
Ｐｉ＋とＰｉ−が特別な形の論理式の場合には．手続きＱで用いるΘの中のＱｉ＋と¬Ｑｉ−の代りにもっと簡単な論理式を使用できる。
【００６２】
Ｐｉ−＝Ｆの場合
Ｐｉの負の述語定義が無い場合には．∀ｘ（¬ｐｉ（ｘ）←Ｆ）が与えられているとみなすことができる。この場合には、Ωを任意の述語の置換とするとＱｉ＋とＱｉ−が前節（Ａ）、（Ｂ）どちらの仕方で決められていても、簡単な計算によって、
Ｑｉ＋Ω≡３  Ｐｉ＋Ωと（¬Ｑｉ−）Ω≡３ＴΩ
が成り立つことがわかる。したがって、補題１よりＱｉ＋と¬Ｑｉ−の代りにそれぞれＰｉ＋とＴを使用できる。
【００６３】
なお、同様にＰｉ＋＝Ｆの場合には、Ｑｉ＋と¬Ｑｉ−の代りにそれぞれＦと¬Ｐｉ−を使用できる。
【００６４】
Ｐｉ−＝¬Ｐｉ＋の場合
これはＰｉ（ｘ）の必要十分条件∀ｘ（ｐｉ（ｘ）←→Ｐｉ＋）が与えられている場合である。
Ωを任意の述語の置換とすると、Ｑｉ＋とＱｉ−が前節（Ａ）、（Ｂ）どちらの仕方で決められていても．簡単な計算によって（Ｑｉ＋Ω≡３Ｐｉ＋Ωと（¬Ｑｉ−）Ω≡３Ｐｉ＋Ωであることがわかる。したがって、この場合には（Ｑｉ＋と¬Ｑｉ−の両方の代りにＰｉ＋を使用できる。なお、Ｑｉ≡３Ｑｉ１１≡３Ｐｉ＋であることも簡単な計算によってわかる。
【００６５】
最後に定理２と他の定理の関係を述べる。
すべてのｉでＰｉ−＝¬Ｐｉ＋の場合に定理２を適用すると、非特許文献２の定理６・３に相当する次の定理が得られる。
［定理］（Ｋｕｎｅｎ）Ｇを任意の閉論理式とする。１次の２つは同値である。
Ｅ（Σ）、∀ｘ（ｐ（ｘ）⇔Ｐ＋）｜＝３Ｇ
∃ｎ  ｓ．ｔ．Ｅ（Σ）｜＝３Ｇ｛Ｐ＋／ｐ｜ｘ｝ｎ｛ｕ／ｐ｝）
また、この２つが成り立つならば
Ｅ（Σ）、∀ｘ（ｐ（ｘ）←→Ｐ＋）｜＝Ｇ
が成り立つ。
【００６６】
また、付録に記したとおり定理２は定理１を用いて証明することができる。
【００６７】
本論文では、論理式の置換手続きと等式のＤＮＦへの変形手続きを組み合わせた論理プログラムの計算手続きの、論理式の置換方法を改良した新しい手続きについて述べた。この手続きは、ＦＬＰの完備化とは異なる完備プログラムの３値論理での論理的帰結を健全かつ完全に判定できることと、ＦＬＰの２値論理での論理的帰結を改良前の手続きよりも多く判定できることを証明し、改良前の手続きと同様に任意のゴールの解の計算結果をＤＮＦの形で表現できることを示した。
【００６８】
上記の手続きで計算できるのは、改良前の計算手続きと同様に、ＦＬＰの論理的帰結のうちの、ＦＬＰから導かれる完備プログラムの３値論理での論理的帰結である。また、本
発明を用いると、否定を含む形式で解を表現できるので、例えばプログラムが｛ｐ（ａ）｝のときの〜Ｐ（ｘ）の解をｘ≠ａと表現できるなどの利点があり、ＮＡＦの解の計算に向いている。ＦＬＰにＮＡＦの使用を導入すると表現力が高まるという利点もあるので、Θ＊を用いた計算手続きでＮＡＦを扱う場合に効果がある。
【００６９】
［付録］
補題１の証明には．次の補題３と４を用いる。
〔補題３〕
Ｅ、φ、ψを論理式とする。Θ＝｛Ｈ／ｐ；Ｇ／ｐ｜ｘ｝を述語の置換とし、Θ’＝｛Ｇ／ｐ；Ｈ／ｐ｜ｘ｝とおく。このとき、
Ｅ｛φ／ｐ；ψ／ｐ｜ｘ｝Θ＝Ｅ｛φΘ／ｐ；ψΘ’／ｐ｜ｘ｝
が成り立つ、
《証明》この補題は、非特許文献１の補題１と同じである。
【００７０】
〔補題４〕
△を開論理式の集合とし、Ｆ＋、Ｆ−、Ｇ＋、Ｇ−をＦ＋∠ΔＴＧ＋かつＦ−∠ΔＦＧ−が成り立つ論理式とする。このとき．任意の閑論理式φに対して
｛Ｆ＋／ｐ；Ｆ−／ｐ｜ｘ｝∠ΔＴφ｛Ｇ＋／ｐ；Ｇ−／ｐ｜ｘ｝
｛Ｆ−／ｐ；Ｆ＋／ｐ｜ｘ｝∠ΔＦφ｛Ｇ−／ｐ；Ｇ＋／ｐ｜ｘ｝
が成り立つ．
《証明》非特許文献１の補題７と同様な手法で証明できる。
【００７１】
《証明》（補題１の証明）、
｛Ｆ＋／ｐ；Ｆ−／ｐ｜ｘ｝ｍ｛ｕ／ｐ｝
｛Ｇ＋／ｐ；Ｇ−／ｐ｜ｘ｝ｍ｛ｕ／ｐ｝
｛Ｆ−／ｐ；Ｆ＋／ｐ｜ｘ｝ｍ｛ｕ／ｐ｝
｛Ｇ−／ｐ；Ｇ＋／ｐ｜ｘ｝ｍ｛ｕ／ｐ｝
をそれぞれΩｍ、Ω’ｍ、Ω＊ｍ、Ω’＊ｍ、と略記する。
ｎに関して帰納的に証明する。
（１）ｎ＝０の婦合、
φΩ０＝φ｛ｕ／ｐ｝＝φΩ’０だから．補題は成り立つ・
（２）ｎ＝ｋの場合
任意の論理式φに対して
ψΩｋ−１∠ΔＴψΩ’ｋ−１かつψΩ＊ｋ−１∠ΔＴψΩ’＊ｋ−１
が成り立つことが証明されていると仮定する。
この仮定と補題１の仮定および、補題３より、
Ｆ＋Ωｋ−１∠ΔＴＦ＋Ω’ｋ−１∠ΔＧ＋Ω’ｋ−１
Ｆ−Ω＊ｋ−１∠ΔＦＦ−Ω’＊ｋ−１∠ΔＦＧ−Ω’＊ｋ−１
が成り立つ．従って、補題４と補題３より、
φΩｎ＝φ｛Ｆ＋Ωｋ−１／ｐ；Ｆ−Ω＊ｋ−１／ｐ｜ｘ｝
∠ΔＴφ｛Ｇ＋Ω’ｋ−１／ｐ；Ｇ−Ω’＊ｋ−１／ｐ｜ｘ｝
φΩ＊ｎ＝φ｛Ｆ−Ω＊ｋ−１／ｐ；Ｆ＋Ωｋ−１／ｐ｜ｘ｝
∠ΔＦφ｛Ｇ−Ω’＊ｋ−１／ｐ；Ｇ＋Ω’ｋ−１／ｐ｜ｘ｝
が成り立つ。ゆえに、補題は成り立つ。
【００７２】
《証明》（補題２の証明）非特許文献１の補題３より、
Ｅ（Σ）｜＝３φ｛ｕ／ｐ｝⇔Ｅ（Σ）｜＝３φ｛Ｆ／ｐ；Ｔ／ｐ｝
が成り立つ。また、ＤＮＦ（φ｛Ｆ／ｐ；Ｔ／ｐ｝）はＴかＦなので、
Ｅ（Σ）｜＝３φ｛Ｆ／ｐ；Ｔ／ｐ｝⇔ＤＮＦ（φ｛Ｆ／ｐ；Ｔ／ｐ｝＝Ｔ
が成り立つ。ゆえに、補題は成り立つ。
【００７３】
《証明》（命題１の証明）
Ωを任意の述語の置換とする。Ｑｉ＋とＱｉ−が（Ａ）、（Ｂ）どちらの仕方で決められていても、簡単な計算によって、
（Ｐｉ＋∧¬Ｐｉ−＋）Ω∠ＴＱｉ＋Ωと
（Ｐｉ＋∨¬Ｐｉ−）Ω∠Ｆ（¬Ｑｉ−）Ω
が成り立つことがわかるので．補題１より本命題が成り立つ。
【００７４】
《証明》（定理２の証明）
Ｑ′＝（Ｑ＋∨ｐ（ｘ））∧（¬Ｑ−∨¬ｐ（ｘ））∧（Ｑ＋∨¬Ｑ−）
Ｑｕ′＝（（Ｑ＋∧¬Ｑ−）∨ｕ）∧（Ｑ＋∨¬Ｑ−）
Θ′＝｛Ｑ＋∧¬Ｑ−／ｐ；Ｑ＋∨¬Ｑ−／ｐ｜ｘ｝
とおく。定理１より次の３式、
Ｅ（Σ）、∀ｘ（ｐ（ｘ）⇔Ｑ′）｜＝３Ｇ
Ｅ（Σ）、∀ｘ（ｐ（ｘ）⇔Ｑｕ′）｜＝３Ｇ
∃ｎ    ｓ．ｔ．  Ｅ（Σ）｜＝３ＧΘ’ｎ｛ｕ／ｐ｝
は同値であり．これらが成り立つならば次の式が成り立つ。
Ｅ（Σ）、∀ｘ（ｐ（ｘ）←Ｑ＋）、∀ｘ（¬ｐ（ｘ）←Ｑ−）｜＝Ｇ
Ωを任意の述語の置換とする、Ｑｉ＋とＱｉ−が（Ａ）、（Ｂ）どちらの仕方で決められていても、簡単な計算によって、
（Ｑｉ＋∧¬Ｑｉ−）Ω≡３Ｑｉ＋Ω
（Ｑｉ＋∧¬Ｑｉ−）Ω≡３（¬Ｑｉ−）Ω
が成り立つことがわかる。したがって、Ｑ≡３Ｑ’とＱｕ≡３Ｑｕ’
が成り立ち、補題１よりＧΘ’ｎ｛ｕ／ｐ｝≡３ＧΘｎ（ｕ／ｐ）が成り立つ
ので、定理の前半が成り立つ。
【００７５】
さらに、Ｑｉ＋とＱｉ−が（Ａ）、（Ｂ）どちらの仕方で決められていても、∀ｘ（ｐ（ｘ）←Ｐ＋）と∀ｘ（¬ｐ（ｘ）←Ｐ−）
のモデルはそれぞれ、
∀ｘ（ｐ（ｘ）←Ｑ＋）と∀ｘ（¬ｐ（ｘ）←Ｑ−）、
のモデルなので、
Ｅ（Σ）、∀ｘ（ｐ（ｘ）←Ｐ＋）、∀ｘ（¬ｐ（ｘ）←Ｑ−）｜＝Ｇ
ならば
Ｅ（Σ）、∀ｘ（ｐ（ｘ）←Ｐ＋）、∀ｘ（¬ｐ（ｘ）←Ｐ−）｜＝Ｇ
が成り立つ。したがって．定理の後半が成り立つ。
【産業上の利用可能性】
【００７６】
本発明の自動定理証明装置では、否定を含む等式で解を表現する自動定理証明装置をつくることができるため、解が「ａ以外」というような場合にａ以外の解を列挙することを避けることができる。
【図面の簡単な説明】
【００７７】
【図１】従来の、導出法による解法例を示す木状の模式図である。
【図２】従来の、タブロー法による解法例を示す木状の模式図である。
【図３】本発明の導出法による解法例を示すための木状の模式図である。
【図４】本発明の導出法による解法例を示すための木状の模式図である。
【図５】本発明の導出法による解法例を従来例に適用した場合の例を示すための木状の模式図である。
【図６】本発明のタブロー法による解法例を示すための木状の模式図である。
【図７】本発明のハードウェアの構成を示す模式図である。
【図８】従来の、導出法による解法例を示すフローチャートである。
【図９】従来の、タブロー法による解法例を示すフローチャートである。
【図１０】本発明の、導出法による解法例を示すフローチャートである。
【図１１】本発明の、タブロー法による解法例を示すフローチャートである。
【符号の説明】
【００７８】
１  入力部
２  演算部
３  記憶部
４  表示部
５  伝送部
【図１】
2005044303.tif 000003
【図２】
2005044303.tif 000004
【図３】
2005044303.tif 000005
【図４】
2005044303.tif 000006
【図５】
2005044303.tif 000007
【図６】
2005044303.tif 000008
【図７】
2005044303.tif 000009
【図８】
2005044303.tif 000010
【図９】
2005044303.tif 000011
【図１０】
2005044303.tif 000012
【図１１】
2005044303.tif 000013