- 著者
-
加藤 雅英
辰己 丈夫
- 雑誌
- 全国大会講演論文集
- 巻号頁・発行日
- vol.50, pp.7-8, 1995-03-15
自動定理証明系の構築に際して問題となるのは、証明が無限に続く時があることと、アラー変数と呼ばれる特殊な変数に自由変数の代入を行なうと、組合せの増加による計算量の増大が起こることである。これに対し我々は、人間と一体になったシステムが証明をすすめることにより、証明が無限に続くことを防ぎ、全体の処理時間を短縮する研究を行なっている。本稿では、論理体系CLCを用いた我々の自動定理証明システムにおいて採用したアラー変数への代入方法が、有効的かつ効率的であることについて述べる。