| 研究課題/領域番号 |
22K11900
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
廣川 直 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (50467122)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2026-03-31
|
| キーワード | 自動演繹 / 項書換え / 定理自動証明 / 停止性 / 完備化 |
|---|
| 研究実績の概要 |
現代の情報社会においてソフトウェアバグは深刻な被害をもたらす。そのためソフトウェアの正しさの保証は社会的な課題となっている。しかし現実社会で用いられるシステムは巨大なものが多く、数学的な証明を自動化する効率的な技法が必要不可欠である。「順序付き完備化」と「書換え帰納法」は、現在最も成功している等式論理の自動証明技法である。これらの証明能力と証明速度を向上させる理論と自動化技法を構築することが本研究の目標である。
令和４年度は、(A)「順序選択問題の解決」と (B)「強力な簡約順序の開発」、また (C)「項書換えの合流性証明技法」の三つに取り組んだ。
(A) 上述の手法を含む現代の自動証明技法は、等式の正しさを証明する際、補題発見と等式変形を繰り返すことで証明を行う。その際、どのように等式変形をしてゆくかを簡約順序と呼ばれる項上の順序で決定している。ここで使用する簡約順序次第で証明が成功するか失敗するかの明暗が分かれ、また証明に要する時間も大きく変化する。この問題解決を図るため、適切な順序を最適化問題によって選出し、自動証明の過程において順序を選定し直せる演繹体系を考案した。
(B) 現在多くの定理自動証明システムは単純化順序と呼ばれる順序を採用している。これは自動化に適しており実装しやすいためであるが、一方でその証明・反証能力の限界にもなっている。この解決のため、重み付き経路順序と呼ばれる簡約順序を一般化する強力な簡約順序を開発した。この順序は自動化に適しており、また単純化順序で証明できない定理を扱える。
(C) 合流性は計算結果の一意性を保証する性質であり、等式の自動証明を計算によって行うことを可能にする。項書換えシステムの合流性を部分システムの合流性に基づいて証明する技法を考案。国際会議 FSCD 2022 において発表した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
開発した手法の評価ため、順序付き完備化の実装を行っている。しかしその効率的な実装には項索引 (term indexing) と呼ばれる技法を導入する必要があり、その実装に時間を要している。一方で理論研究は計画以上の進捗を得ており、全体としてはおおむね順調に進展しているといえる。
|
| 今後の研究の推進方策 |
今後は実験評価を繰り返しながら、開発した手法を洗練・拡張させてゆく。多くの対話的定理証明システムは高階論理に基づいているが、それに適した自動演繹の体系の構築に取り組む。
|
| 次年度使用額が生じた理由 |
次年度以降の配分額では成果発表ための学会出張が困難であるため、研究機材を購入を断念した。学会参加の旅費に使用する。
|
