定理証明・自動推論に関する研究　

−△−▽−△−名古屋工業大学大学院研究情報工学専攻伊藤研との共同研究 −△−▽−△−　　　 　　

　

　研　究　の　目　的
    すべての人工知能問題は自動推論に帰着すると言われている． 一階述語定理証明・自動推論は自動推論の分野において 最も重要な要素の一つである．定理証明・自動推論の進歩はコンピュータサイエンスだけではなく、 すべての科学技術と社会生活の進歩につながる．本研究では定理証明や自動推論の効率に 関連する問題に対する効率的な手法を提案することによって，定理証明・自動推論の発展に貢献する．

  1. エルブラン定理の改良

    2. 　1930年に22歳のフランスの数学家エルブラン（1931年23歳の若さで登山事故で他界にした） が提案したエルブラン定理 はほとんどの自動定理証明と自動推論方法の基礎となっている．与えられた節集合（推論ルールの 集合）が充足不能であることを示す（証明する）には，あらゆる対象領域のあらゆる解釈を考えなければならない． これは事実上不可能である．幸いなことに，充足不能であることを論じる上であらゆる対象領域と等価な1つの 対象領域が存在する．それは，エルブラン領域（Herbrand universe)と呼ばれるものである．

    エルブラン領域：　節集合S のエルブラン領域H(S)は次のように構成的に定義される．

    1. H0 ={節集合Sに現れる個体定数の集合}　

      2. 　もし節集合Sに個体定数がなければ，任意の定数を1つとって，たとえば，それをc として　
      H0 ={c }
      とする． 　　
    2. i=0,1,2,3,... に対して　

      3. 　 　　　
      Hi+1= HiU{f　(t1, t2, ...., tn)の集合}
      ここでf はSに現れるすべての関数をとり，t1, t2, ...., tnはHi のすべての要素をとる．

    例えば，次の節集合を考える． 　　
    ¬p(c).
    ¬q(f (c)).
    p(X)Vq(X).
    この節集合のエルブラン領域H は次のようになる. 　　
    H ={c, f (c), f (f (c)), f (f (f (c))), .......}
    H は無限個の要素をもつことにご留意.

    基礎アトムと基礎節： 変数を含んでいないアトムを基礎アトムという．節集合 S 中の任意の節 Cに含まれる変数にエルブラン領域の要素を代入 してできる節をS の基礎節という．

    エルブランの定理：　節集合S が充足不能であるための必要十分条件は， S の基礎節のある有限集合が充足不能であることである．
    　
    エルブランの定理の問題点：　エルブランの定理が提案されてから，77年間そのまま継承されて きた．しかし，エルブラン領域は節集合の充足不能を証明するための充分な領域であるが，必要な領域ではない． 問題によっては，必要な要素が有限個なのに，エルブラン領域が無限に なっていることもある．例えば，上の例では，変数Xにおいて，無限なエルブラン領域　{c, f (c), f (f (c)), 　f (f (f (c))), .......} ではなく，｛c, f (c)} をだけ考えれば十分である．
    　
    エルブランの定理の改良：　エルブラン定理の問題点を解決するために，我々はエルブランの定理の改良 を提案した[1], [2]．エルブラン領域では，節集合にあるすべての変数を対象としているに対して，我々は 変数ごとに，その変数に対応するエルブラン領域を計算する．このように計算して得られたエルブラン領域は元の エルブラン領域の子集合であるため，サブエルブラン領域と呼ぶことにする．我々は， 節集合S が充足不能であるための必要十分条件は， S の各変数に対してその変数に対応するサブエルブラン 領域の要素を代入して得られる基礎節のある有限集合が 充足不能であるということを証明した．我々の方法では，上の例において，変数Xに対応する サブエルブランは｛c, f (c)} となる．
    　
    応用の一例：　前向き推論定理証明器SATCHMOは，領域限定（節の本体（結論）に現れる変数 は節の頭部（前提）にも現れる節は領域限定節という）である節集合S の 充足可能性を 判定するために，空集合からS の各節を順番に充足させながら， S のモデルを求めていく． S のすべての節を充足する モデルを発見できれば，S は充足可能であり，そうでなければ， S は充足不能である．
    　 任意の非領域限定節集合は領域限定節集合に変換することができるが，そのとき， 非領域限定変数(節の本体（結論）にしか現れない変数)が領域限定変換によって エルブラン領域に基礎化される．エルブラン領域に証明に無用な要素が存在すれば， 不効率な要因になる．例えば，上の例では，SATCHMOはS のすべての要素 を試していき，無限のループに落ちいて証明をあげることができない．
    　我々の改良によって，特定の変数を，その変数と関連のあるサブエルブラン領域だけ 基礎化するため，無駄な推論を防ぐことができる．
    　定理証明のベンチマーク問題集 TPTP ライブラリ[3]version 2.5.0 には， 5181問が存在する．その中の2881問は非領域限定かつ非ホー ン節を含む問題である．本稿で提案した手法が適用できる問題，すなわち，2つ 以上の$SHU$が導出される問題の数は451である．導出された最大のサブエルブラン 領域の数は271である（問題 SYN837-1）． 例えば， TPTP ライブラリに次の問題（PUZ017-1.p）がある.　
    There are 5 houses, 5 people, 5 colors, 5 drinks, 5 games, and 4 pets. Each house has a person, a color, a drink, and game, and all but one of the houses has a pet. The problem is to match each house with as many properties as possible. House 1 is at the left end and house 5 is at the right end. The Englishman lives in the Red house. The white house is left of the Green house. The Italian has a Guppy. Lemonade 　　　 is drunk in the Green house. The Swede lives in the house where Coffee is drunk. The Toad lives in the house where Backgammon is played. Racquetball is played in the yellow house. Milk is drunk in the third house. The Russian lives in the first house. The Camel lives next to the house where Quoits is played. The Rat lives next to the house where Racquetball is played. Solitaire is played in the house where vodka is drunk. The American lives in the house where Charades is played. The Russian lives next to the Blue house.
    この問題のエルブラン領域H は次のようになる．

    H = {house1, house2, house3, house4, house5, no_pet, rat, camel, toad, guppy, charades, solitaire, quoits, racquetball, backgammon, unknown_drink, vodka, milk, coffee, lemonade, blue, yellow, green, white, red, american, russian, swede, italian, englishman}　

    この問題には，次のような非領域限定節がある．

    true →hasdrink(house1, A);hasdrink(house2, A);hasdrink(house3, A);hasdrink(house4, A);hasdrink(house5, A).
    　
    通常の領域限定変換によると，上記の節は次の領域限定節になる．　

    dom(A) →hasdrink(house1, A);hasdrink(house2, A);hasdrink(house3, A);hasdrink(house4, A);hasdrink(house5, A).
    　
    ただし，Aはエルブラン領域のすべての要素をとる．そのため，無意味な基礎節が多数生成されてしまう． 例えば，Aがエルブラン領域の要素ratをとる場合，hasdrink(house1, rat)はまったく意味のないものである． なぜならば，ratはペットであり，飲み物ではないからである．同様に，Aは各 house,　各people, 各color,　 各pet および各gameの値をとるときも，無意味な基礎節になる．その結果， Intel PentiumIII/980MHZ ワークステーションの上で，SATCHMO関連のすべての証明システムは1時間 内にこの問題を解決できない．
    我々の改良を用いれば，次の6つのサブエルブラン領域を導出できる．
    H1 = {house1, house2, house3, house4, house5}
    H2 = {no_pet, rat, camel, toad, guppy}
    H3 = {charades, solitaire, quoits, racquetball, backgammon}
    H4 = {unknown_drink, vodka, milk, coffee, lemonade}
    H5 = {blue, yellow, green, white, red}
    H6 = {american, russian, swede, italian, englishman}
    　 各サブエルブラン領域は同じ性質をもつ要素の集合になっていることを留意してほしい．
    上記の非領域限定節にある変数Ａに対応するサブエルブランはＨ4である．Ｈ4 の要素だけをとる補助述語dom4を用いれば，次の領域限定節に変換できる．

    dom4(A) →hasdrink(house1, A);hasdrink(house2, A);hasdrink(house3, A);hasdrink(house4, A);hasdrink(house5, A).
    　
    これにより，ＳＡＴＣＨＭＯでも，Intel PentiumIII/980MHZ ワークステーションの上で， この問題の証明を1秒内に終えることができた．
    　
    [1] 何 立風, 巣 宇燕, 川那 宜充, 加藤 昇平, 中村 剛士, 伊藤 英則, サブエルブラン領域の特定 およびモデル生成定理証明への応用, 情報処理学会論文誌, Vol.46, No.5, 2004年6月.
    [2] Y. Chao, Lifeng He, Z. Shi, K. Suzuki, T. Nakamura, H. Itoh, An Improvement of Herbrand Theorem and Its Application to Model Generation Theorem Proving, Journal of Computer Science and Technology, Vol. 22, No. 4, pp.xxx-yyy, 2007. (accepted).
    [3] Sutcliffe, G. and Suttner, C.: http://www.cs.miami.edu/~tptp/

  2. 前向き推論の効率化

    3. 　一階述語自動推論の手法として後向き推論（Backward chaining reasoning) と前向き 推論 (Forward chianing reasoning) がある．後向き推論では，推論の目標からその目標を導出する必要な直接の前提 を見つけ出し，そして，それらの前提を新たな目標とし，それら新たな目標を導出する必要な前提を見つけ出す．これらの 操作は繰り返して行い，すべての前提が与えれた事実であることになれば，推論目標は与えられた事実と推論ルールから 推論（証明）できるという．そうでなければ，推論目標は与えられた事実と推論ルールから推論（証明）できないという．これに 対して，前向き推論は与えられた事実が前提を満たす推論ルールに適応し，新たな事実を導出する．そして，新たな事実をこれまでの 事実に加え，これらの事実が前提を満たせるルールにより，さらに新たな事実を導出する．このような操作を繰り返し行い，目標は事実として導出できれば，推論目標は与えられた事実と推論ルールから 推論（証明）できる．推論目標は新しい事実を導出できないまでも 導出できない場合，推論目標は与えられた事実と推論ルールから 推論（証明）できない．
    　これまでは，後向き推論は主流手法として利用してきたが，最近，前向き推論器SATCHMO1の推論原理が簡単，実装しやすい，人間の推論方法に近いなど利点から，注目されしつつである。
    　前向き推論では，推論ルールの前提が充足され，結論が充足されないルールを前向き推論に用いる．そのため， 証明に関連のない非ホーン節（非ホーン節とは，複数の結論を選言にもつ推論ルールである）が存在する場合には， 探索空間が爆発的に増大することがある．
    　証明に関連がある非ホーン節だけを推論に用いれば，無駄な探索が防げることが 明らかできる．そのため，非ホーン節を選ぶ基準として，我々は 「関連性」(relevancy)の概念を導入したSATCHMORE2に， 「有用性」(availability)の概念を組み込んだ A-SATCHMORE3 を提案した．
    　しかるに, 関連があると認識された非ホーン節は実際の推論に 関連でないことがある. そのとき, 探索空間は無駄に広げられてしまう場合がある．そこで， 我々はモデル生成法に向けの新たな効率化手法組み込んだ 定理証明器 I-SATCHMO4や R-SATCHMO5を提案した． I-SATCHMO では, SATCHMO と同様, 最初に発見した 違反節を前向き推論に用いる. ただし, 推論に用いた非ホーン節 の頭部アトムが推論に貢献するかどうかによってその非ホーン節 が推論に必要かどうかを判断する. 推論に貢献しない頭部アトムを もつ非ホーン節は証明に関連がない. 従って, 処理中の違反節の頭部 アトムは有用でないと判断された時点でその節に対する処理を 削除できる. このように，無駄な探索を防止し, 証明の効率化を実現している. R-SATCHMOでは, 部分推論を結果を定理としてまとめて推論ルールに加える． それによって，重複な推論を防ぐことができる．
    　
    [1] R. Manthey and F. Bry: SATCHMO: a theorem prover implemented in Prolog. Proceedings of 9th Conference on Automated Deduction, Argonne, Illinois, USA, 1988, pp.415-434.　
    [2] D.W. Loveland, D.W. Reed and D.S. Wilson: SATCHMORE: SATCHMO with RElevancy, Journal of Automated Reasoning, 14: 325-351, 1995.
    [3] Lifeng He , Y. Chao, Y. Shimajiri, H. Seki, H. Itoh, A-SATCHMORE: SATCHMORE with Availability checking, Journal of New Generation Computing, pp.55-74, Vol. 16, 1998.
    [4] Lifeng He : I-SATCHMO: An Improvement of SATCHMO. Journal　of Automated Reasoning, Vol.40 No.6, pp. 313-322, 2001.
    [5] Lifeng He, Y. Chao, H. Itoh: R-SATCHMO: Refinements on I-SATCHMO. Journal of Logic and computation, Vol.14, No. 2, pp.117-143, 2004.

    研究紹介にもどる

    日本語TOP English TOP 中国語 TOP