MGTP による有限代数の新事実の発見

概要

論文の詳細を見る
本稿では,定理証明器MGTPによって解いて準群に関する未解決問題とそこで用いたヒューリスティックスならびに並列化について報告する.有限代数の存在問題はコンピュータを利用した数え上げによる証明が有望な研究分野であるが,ただ単純に数え上げを行っただけでは,探索空間の爆発により証明が因難である.有限準群の存在問題もその例に洩れず,これまで定理証明システムによる適用はごく限られていた.本研究では,準群問題に対しモデル生成法と呼ばれる定理証明手法を適用し,探索候補の選択に関連したヒュリスティックスを導入することによって探索空間の削減を行った.モデル生成法は場合分けによるOR並列化が容易であり,ここで導入したような探索木の枝刈り戦略とは互いにその効果を損なわないという特長を持つ.本研究で得られた結果は,準群問題が非ホーン節で簡単に表現できたことと,導入した枝刈り戦略およびこうしたモデル生成法の特長が本質的であった.ただし,MGTPおよびここで与えた手法は準群問題を証明するために特化したものではなく,他の非ホーン表現の探索問題にも適用が期待できる.一方,準群問題は実験計画法などへの応用を持つブロック問題と深い関連を持つ.本研究の結果はそうした分野への定理証明の応用可能性を示唆したと考えられる.
一般社団法人情報処理学会の論文
1994-07-15

MGTP による有限代数の新事実の発見

スポンサーリンク

概要

著者

関連論文

スポンサーリンク