研究テーマ：自動定理発見
はじめに_
この研究テーマは先端情報システム工学研究室で行っています。
自動定理発見問題_
自動定理発見（Automated Theorem Finding, ATF）とは，予め与えられた定理を自動的に証明することではなく，計算機を用いて新しい定理を自動的に発見することである．自動定理発見問題（Automated Theorem Finding Problem）は，自動定理発見の一般的な方法を求めるという問題であり，1988年ごろ自動定理証明の大家であるアメリカのWos博士により提示された世界的に知られている難問である (Wos 1988)．
この問題が完全に解決されれば，いろいろな科学技術分野で非常に多くの応用があるため，多くの計算機科学者は様々な角度からその解決に挑戦してきたが，今現在もまだ完全に解決されていない．
自動定理発見と自動定理証明_
自動定理証明（Automated Theorem Proving, ATP）に有効な従来の後向き（証明しようとする定理を利用して前提まで辿り着くこと）証明法は自動定理発見に全く適用できない．「推論」とは，与えられた前提（既知の事実あるいは仮定）に推論規則を適用して未知の新しい結論を導出する過程のことである．一方，「証明」とは，あらかじめ明確に与えられた結論（言明あるいは仮説）に対して，与えられた前提（既知の事実あるいは仮定）からその結論へ至る論理的道筋を見つけ出す過程のことである．
推論と証明の本質的な違いは，証明は証明しようとする物事（ゴール）があらかじめ既に定まっていることに対して，推論は推論すべき物事（ゴール）があらかじめ定まっていないことにある．自動定理発見は自動定理証明と異なり，予めゴール，すなわち発見すべき定理を定めることができないため，証明では行うことができず，推論を用いるしかない． このため，従来の後向き証明法は自動定理発見に全く適用できない．
また，従来のほとんどの自動定理証明系で論理基礎として採用されてきた古典数理論理（Classical Mathematical Logic）も，自動定理発見にとって適切ではない．古典数理論理とその拡張論理には，条件関係「もし・・・ならば～」を表す論理結合子として実質含意が定義されているが，われわれが普段用いる「もし・・・ならば～」の意味と実質含意の意味が異なる．このため，古典数理論理とその拡張論理には，われわれの常識からみれば不自然な論理定理（これを，実質含意のパラドクスという）を含んでおり，古典数理論理に基づく推論を行うと，われわれにとって不自然な結論が導出される可能性がある (Anderson and Belnap Jr. 1975; Anderson et. al 1992)．また，古典数理論理の論理定理には実質含意のパラドクスが大量に含まれていることが定量的に実証されている (Goto and Cheng 2007)．
強相関論理に基づく前向き推論を用いた自動定理発見_
これらの二つの問題を解決するために，程によって，強相関論理に基づく前向き推論を用いた自動定理発見の理論的基礎と方法が提案された (Cheng 1994)．この方法では，古典数理論理とその拡張論理に含まれる実質含意のパラドクスをすべて排除した論理体系である強相関論理 (Cheng 2000, 2006) に基づき，前向き推論により定理を自動的に導出し，導出した定理の中から新しく，かつ，面白い定理の候補を自動的に絞り込み、そのあと、数学者や利用者と協調して新しく，かつ，面白い定理を発見する．
この方法の特徴は，推論の妥当性を基礎付ける論理体系とそれぞれの分野の定義・公理・定理，また，それら二つの入力から新たな定理の導出を行う推論プログラムを明確に分離した点にある．程は，推論の妥当性を基礎付ける論理体系として強相関論理を選んだが，一般的には，定理発見を行いたい分野や推論の妥当性や扱いたい概念は，自動定理発見の実行者によって異なると考えられる．このため，推論の妥当性を基礎づける論理体系と推論プログラムは分離されていなければならない．提案方法に従えば，実行者が妥当と思う論理体系と，定理発見を行いたい分野の定義や公理，定理を自由に入力として与えられる．このため，汎用的にかつ，統一的な手法により自動定理発見を行うことができる．
提案方法を実現するためには，使用したい論理体系を入力データとして用意すること，また，定理発見を行いたい分野の定義と公理，定理を入力データとして用意すること，そして，任意の論理体系，任意の分野の定義と公理と定理を扱える推論プログラムを用意する必要がある．このような推論プログラムとして，汎用前向き推論エンジンFreeEnCalが提案され，開発されている (Cheng et al. 2008; Koh et al. 2008, 2010; Goto et al. 2008, 2012)．
NBG集合論における自動定理発見の事例研究_
高らによって，強相関論理に基づく前向き推論を用いた自動定理発見の具体的な手法が提案され，その手法の有効性を確かめるためにNBG集合論における事例研究が行われた (Gao et al. 2014)．この事例研究において，既知の定理を本手法によって導出することができた（再発見できた）．このことから，より時間と計算資源を費やすことで，未知の定理の発見を行う可能性があることがわかった．
現状と今後の課題_
強相関論理に基づく前向き推論を用いた自動定理発見手法が原理的には自動定理発見問題の解決に有用であることが，NBG集合論における事例研究で確認できた．しかし，実際に数学の新たな定理を計算機で自動発見すること，また，自動定理発見問題を解決したといえる方法およびその方法に基づく環境の構築までは，まだまだ挑戦的な課題が多く残っている．
- より多くの定理を導出するため，汎用前向き推論エンジンFreeEnCalの性能をどのように向上させていけばよいのか？
- 汎用前向き推論エンジンFreeEnCalで導出された膨大な定理のなかから「新しく」かつ「面白い」定理をどのように抽出すればよいか？
- 「新しく」かつ「面白い」定理を導出するために，自動定理発見プロセスにおいてどのような操作が必要か？
- 任意の数学分野，また，数学以外の分野の定理発見を行うために，どのような仕組みが必要となるのか？それをどう構築すればよいのか？
参考文献_
- (Anderson and Belnap Jr. 1975)
Anderson, A.R., Belnap Jr., N.D., Entailment: The Logic of Relevance and Necessity, vol.1, Princeton University Press, 1975.
- (Anderson et. al 1992)
Anderson, A.R., Belnap Jr., N.D., Dunn, J.M., Entailment: The Logic of Relevance and Necessity, vol.2, Princeton University Press, 1992.
- (Cheng 1994)
Cheng, J., A Relevant Logic Approach to Automated Theorem Finding, Proc. Workshop on Automated Theorem Proving attached to International Symposium on Fifth Generation Computer Systems 1994, pp. 8-15, Tokyo, Japan, 1994.
- (Cheng 2000)
Cheng, J., A Strong Relevant Logic Model of Epistemic Processes in Scientific Discovery, in E. Kawaguchi, H. Kangassalo, H. Jaakkola, and I. A. Hamid (Eds.), "Information Modelling and Knowledge Bases XI," Frontiers in Artificial Intelligence and Applications, Vol. 61, pp. 136-159, IOS Press, 2000.
- (Cheng 2006)
Cheng, J., Strong Relevant Logic as the Universal Basis of Various Applied Logics for Knowledge Representation and Reasoning, in Y. Kiyoki, J. Henno, H. Jaakkola, and H. Kangassalo (Eds.), "Information Modelling and Knowledge Bases XVII," Frontiers in Artificial Intelligence and Applications, Vol. 136, pp. 310-320, IOS Press, 2006.
- (Cheng et al. 2007)
Cheng, J., Nara, S., Goto, Y., FreeEnCal: A Forward Reasoning Engine with General-Purpose, in B. Apolloni, R. J. Howlett, and L. C. Jain (Eds.), "Knowledge-Based Intelligent Information and Engineering Systems, 11th International Conference, KES 2007, XVII Italian Workshop on Neural Networks, Vietri sul Mare, Italy, September 12-14, 2007, Proceedings, Part II," Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science), Vol. 4693, pp. 444-452, Springer-Verlag, 2007.
- (Gao et al. 2014)
Gao, H., Goto, Y., Cheng, J. ,A Systematic Methodology for Automated Theorem Finding, Theoretical Computer Science, Vol. 554, pp. 2-21, Elsevier B.V., October 2014.
- (Goto and Cheng 2007)
Goto, Y., Cheng, J., A Quantitative Analysis of Implicational Paradoxes in Classical Mathematical Logic, Electronic Notes in Theoretical Computer Science, "Proceedings of the Workshop on Logic, Model and Computer Science (LMCS06), Camerino, Italy, 20-22 April 2006," Vol. 169, pp. 87-97, Elsevier B.V., 2007.
- (Goto et al. 2008)
Goto, Y., Koh, T., Cheng, J., A General Forward Reasoning Algorithm for Various Logic Systems with Different Formalizations, in I. Lovrek, R. J. Howlett, and L. C. Jain (Eds.), "Knowledge-Based Intelligent Information and Engineering Systems, 12th International Conference, KES 2008, Zagreb, Croatia, September 3-5, 2008, Proceedings, Part II," Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science), Vol. 5178, pp. 526-535, Springer-Verlag, 2008
- (Goto et al. 2012)
Goto, Y., Gao, H., Tsuji, T., Cheng, J., Practical Usage of FreeEnCal?: an Automated Forward Reasoning Engine for General-Purpose, Proceedings of the International Conference on Machine Learning and Cybernetics (ICMLC 2012), pp. 1878 - 1883, Xi'an, China, IEEE Press, 2012.
- (Koh et al. 2008)
Koh, T., Goto, Y., Cheng, J., A Fast Duplication Checking Algorithm for Forward Reasoning Engines, in I. Lovrek, R. J. Howlett, and L. C. Jain (Eds.), "Knowledge-Based Intelligent Information and Engineering Systems, 12th International Conference, KES 2008, Zagreb, Croatia, September 3-5, 2008, Proceedings," Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science), Vol. 5178, pp. 499-507, Springer-Verlag, 2008.
- (Koh et al. 2010)
Koh, T., Goto, Y., Cheng, J., A Fast Algorithm for Derivation Process in Forward Reasoning Engines, International Journal of Computational Science, Vol. 4, No. 3, pp. 219-231, Global Information Publisher, 2010.
- (Wos 1988)
Wos, Automated Reasoning 33 Basic Research Problems, 1988.