Automated Deduction and Reduction Orders

点击翻译按钮获取中文摘要

現代の情報社会においてソフトウェアバグは深刻な被害をもたらす。そのためソフトウェアの正しさの保証は社会的な課題となっている。しかし現実社会で用いられるシステムは巨大なものが多く、数学的な証明を自動化する効率的な技法が必要不可欠である。「順序付き完備化」と「書換え帰納法」は、現在最も成功している等式論理の自動証明技法である。これらの証明能力と証明速度を向上させる理論と自動化技法を構築することが本研究の目標である。令和４年度は、(A)「順序選択問題の解決」と (B)「強力な簡約順序の開発」、また (C)「項書換えの合流性証明技法」の三つに取り組んだ。(A) 上述の手法を含む現代の自動証明技法は、等式の正しさを証明する際、補題発見と等式変形を繰り返すことで証明を行う。その際、どのように等式変形をしてゆくかを簡約順序と呼ばれる項上の順序で決定している。ここで使用する簡約順序次第で証明が成功するか失敗するかの明暗が分かれ、また証明に要する時間も大きく変化する。この問題解決を図るため、適切な順序を最適化問題によって選出し、自動証明の過程において順序を選定し直せる演繹体系を考案した。(B) 現在多くの定理自動証明システムは単純化順序と呼ばれる順序を採用している。これは自動化に適しており実装しやすいためであるが、一方でその証明・反証能力の限界にもなっている。この解決のため、重み付き経路順序と呼ばれる簡約順序を一般化する強力な簡約順序を開発した。この順序は自動化に適しており、また単純化順序で証明できない定理を扱える。(C) 合流性は計算結果の一意性を保証する性質であり、等式の自動証明を計算によって行うことを可能にする。項書換えシステムの合流性を部分システムの合流性に基づいて証明する技法を考案。国際会議 FSCD 2022 において発表した。