2022 Fiscal Year Research-status Report
Automated Deduction and Reduction Orders
| Project/Area Number |
22K11900
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
廣川 直 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (50467122)
|
|---|
| Project Period (FY) |
2022-04-01 – 2026-03-31
|
| Keywords | 自動演繹 / 項書換え / 定理自動証明 / 停止性 / 完備化 |
|---|
| Outline of Annual Research Achievements |
現代の情報社会においてソフトウェアバグは深刻な被害をもたらす。そのためソフトウェアの正しさの保証は社会的な課題となっている。しかし現実社会で用いられるシステムは巨大なものが多く、数学的な証明を自動化する効率的な技法が必要不可欠である。「順序付き完備化」と「書換え帰納法」は、現在最も成功している等式論理の自動証明技法である。これらの証明能力と証明速度を向上させる理論と自動化技法を構築することが本研究の目標である。
令和４年度は、(A)「順序選択問題の解決」と (B)「強力な簡約順序の開発」、また (C)「項書換えの合流性証明技法」の三つに取り組んだ。
(A) 上述の手法を含む現代の自動証明技法は、等式の正しさを証明する際、補題発見と等式変形を繰り返すことで証明を行う。その際、どのように等式変形をしてゆくかを簡約順序と呼ばれる項上の順序で決定している。ここで使用する簡約順序次第で証明が成功するか失敗するかの明暗が分かれ、また証明に要する時間も大きく変化する。この問題解決を図るため、適切な順序を最適化問題によって選出し、自動証明の過程において順序を選定し直せる演繹体系を考案した。
(B) 現在多くの定理自動証明システムは単純化順序と呼ばれる順序を採用している。これは自動化に適しており実装しやすいためであるが、一方でその証明・反証能力の限界にもなっている。この解決のため、重み付き経路順序と呼ばれる簡約順序を一般化する強力な簡約順序を開発した。この順序は自動化に適しており、また単純化順序で証明できない定理を扱える。
(C) 合流性は計算結果の一意性を保証する性質であり、等式の自動証明を計算によって行うことを可能にする。項書換えシステムの合流性を部分システムの合流性に基づいて証明する技法を考案。国際会議 FSCD 2022 において発表した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
開発した手法の評価ため、順序付き完備化の実装を行っている。しかしその効率的な実装には項索引 (term indexing) と呼ばれる技法を導入する必要があり、その実装に時間を要している。一方で理論研究は計画以上の進捗を得ており、全体としてはおおむね順調に進展しているといえる。
|
| Strategy for Future Research Activity |
今後は実験評価を繰り返しながら、開発した手法を洗練・拡張させてゆく。多くの対話的定理証明システムは高階論理に基づいているが、それに適した自動演繹の体系の構築に取り組む。
|
| Causes of Carryover |
次年度以降の配分額では成果発表ための学会出張が困難であるため、研究機材を購入を断念した。学会参加の旅費に使用する。
|
-
[Presentation] Compositional Confluence Criteria2022
Author(s)
Kiraku Shintani and Nao Hirokawa
Organizer
Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics, 2022.
Int'l Joint Research
-
-
