| 研究課題/領域番号 |
25540003
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
小川 瑞史 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40362024)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | 定理証明系 / 形式証明 / 項書換え系 |
|---|
| 研究実績の概要 |
H26年度においては、定理証明系Isabelle/HOL による形式証明の実装にかわり、証明変換系の基礎となる項書換え系における新たな合流性の十分条件について、研究を進めた。項書換え系の合流性は、計算結果の一意性や等式論理における無矛盾性を示す十分条件である。項書換え系が停止しない場合、左線形な場合については1970年代より主要な十分条件が知られていたが、左非線形の場合については、未解決問題が多く残っている。その中で、左線形にかわり右線形を仮定する未解決問題（1990年に提示された）「強無曖昧かつ右線形な項書換え系は合流性を持つ」に挑戦し、リダクショングラフに基づく新たな証明手法を開発し、「強無曖昧かつ弱浅性を持つ項書換え系は合流性を持つ」を示した（第25回自動推論国際会議 H27年8月ベルリン開催にて採録・発表予定）。この手法は、従来の等式証明上に整礎順序を発見的に構成する証明手法に対し、書換え関係の有限部分集合であるリダクショングラフを変形・拡大することで合流する書換え列を構成する革新的なものであり、上記、未解決問題における重要なステップと自負している。
また、パリ第六大学滞在中（H26年9月～10月）に Jean-Pierre Jouannaud 教授（Ecole Polytech) らと共同で、異なるアプローチによる左非線形な項書換え系の合流性の十分条件を提案した。これは、rank とよばれるリデックスのネストの回数に注目し、rank-increasing であれば、書換えの系列は階層化される。これは、階層化が保存される限り、ω曖昧なcritical pair を含む場合についても拡張が可能な柔軟な条件となっている。（現在、国際会議 CSL2015 に投稿中。）なお、これら二つの結果は互いに独立である。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
現在までに、項書換え系の合流性に対し、リダクショングラフに基づく革新的な証明手法を提案することができたが、本研究提案の主題に対しては周辺的な技術が必要である。数学的な定理・補題の形式証明については遅れがでている現状である。この一因は、当初、学生雇用により、形式証明の定理証明系上での実装を進める予定であったが、学生にはハードルが高く、H27年度は、学生雇用のみならず、研究代表者による形式証明実装を進める予定である。
|
| 今後の研究の推進方策 |
最終年度（H27年度）は、(1)左非線形な項書換え系の合流性の十分条件について、リダクショングラフに基づく証明手法による、さらなる拡張、および (2) Lovasz の補題をターゲットにした定理証明系 Isabelle/HOL上の形式証明の実装とその証明項の変換についてのケーススタディを進める。Higman の補題については、Monika Seisenberger らが既に研究を進めており、まだ試みられていない Lovasz の補題をターゲットとする。特に、Lovaszの補題は、命題論理の積和標準形の充足可能性を確率的に保証する応用が知られており、確率的な充足可能インスタンスの存在と具体的な充足可能インスタンスの構成に差があり、古典証明における計算可能性について、適切なケーススタディと考えている。
|
