| 研究課題/領域番号 |
22K11900
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60010:情報学基礎論関連
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
廣川 直 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (50467122)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2026-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
3,770千円 (直接経費: 2,900千円、間接経費: 870千円)
2025年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2024年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2023年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2022年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
|
|---|
| キーワード | 自動演繹 / 項書換え / 定理自動証明 / 停止性 / 完備化 / 簡約順序 |
|---|
| 研究開始時の研究の概要 |
現代の情報社会においてソフトウェアバグは深刻な被害をもたらす。そのためソフトウェアの正しさの保証は社会的な課題となっている。しかし現実社会で用いられるシステムは巨大なものが多く、人手による検証は現実的ではない。そのため必要とされる数学的な証明を自動化する効率的な技法が必要不可欠である。1989年に登場した順序付き完備化は、現在最も成功している等式論理の自動証明技法である。この証明能力と証明速度を向上させる理論と自動化技法を研究する。
|
| 研究実績の概要 |
現代の情報社会においてソフトウェアバグは深刻な被害をもたらすため、ソフトウェアの正しさの保証は社会的な課題となっている。しかし現実社会で用いられるシステムは巨大なものが多く、数学的証明を効率的に自動化する技法が必要不可欠となる。「順序付き完備化」と「書換え帰納法」は、現在最も成功している等式論理の自動証明技法である。これらの証明能力と証明速度を向上させる理論と自動化技法を構築することが本研究の目標である。令和４年度に引き続き、(A)「順序選択問題の解決」、(B)「強力な簡約順序の開発」、「項書換えの合流性証明技法」の三つに取り組んだ。
(A) 結合律 (x+y)+z=x+(y+z) と交換律 x+y=y+x を満たす演算子はAC演算子と呼ばれる。数学定理やソフトウェア検証における多くの命題には算術が関与し、AC演算子を扱う必要がある。自動演繹の基本は、0+x=x のような等式を計算規則 0+x→x として扱い数式を単純化することにあるが、AC演算子は0+x→x+0→0+x→…のように素朴な単純計算方法では停止しないため、それらを扱う「AC完備化」と呼ばれる手法が研究されている。本研究では既存の３つのAC完備化を調査し、それらの証明能力が階層を為すことを解明した。
(B) 現在多くの定理自動証明システムは簡約順序と呼ばれる順序を用いて、等式を計算規則にする際の矢印の向きを決めている。AC演算子を扱え、かつ理論的な扱いが容易な新たな簡約順序を開発した。
(C) 合流性は計算結果の一意性を保証する性質であり、等式の自動証明を計算によって行うことを可能にする。令和４年度の成果を深化させ、項書換えシステムの合流性を部分システムの合流性に還元する技法を開発、論文誌 LMCS 2022 において発表した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
自動証明において結合律・交換律を扱う基盤技術の研究を行い、当初の予定以上の成果を得た。一方で定理自動証明のための項索引の実装に想定以上の時間を要しており、全てが順調というわけではない。しかし概ねは順調に進展しているといえる。
|
| 今後の研究の推進方策 |
次年度は基本的に高階論理の自動演繹の研究に取り組むが、当該年度に得られた成果は萌芽的な成果が多く多分に改良の余地を残しているため、それら成果の深化も並行して行う。
|
