Automated Deduction and Reduction Orders

自动扣除和减少订单

基本信息

批准号：
22K11900
负责人：
廣川直
金额：
$ 2.41万
依托单位：
Japan Advanced Institute of Science and Technology
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2022
资助国家：
日本
起止时间：
2022-04-01 至 2026-03-31
项目状态：
未结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22K11900/
关键词：
自動演繹項書換え定理自動証明停止性完備化簡約順序

项目摘要

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

软件错误在现代信息社会中造成严重破坏。因此，确保软件的正确性是一个社会问题。但是，现实生活中使用的许多系统都是巨大的，自动化数学证明的有效技术至关重要。 “订购已完成”和“重写归纳”目前是方程逻辑最成功的自动证明技术。这项研究的目的是构建提高这些证明功能和证明速度的理论和自动化技术。在2022财政年度，我们研究了三个主题：（a）“解决订单选择问题”，（b）“开发强大的简化订单”和（c）“用于证明术语重写的汇合的方法”。（a）现代自动证明技术，包括上述方法，在证明方程式的正确性时，通过重复引理发现和方程转换来执行证明。在这种情况下，如何通过术语按顺序确定方程式，称为简化顺序。根据此处使用的简化顺序，证明成功还是失败的亮度和黑暗将有所不同，以及证明更改所需的时间。为了解决此问题，我们设计了一个扣除系统，该系统允许使用优化问题选择适当的顺序，并在自动证明过程中重新选择订单。（b）许多自动定理证明系统现在采用称为简化顺序的订单。这是因为它适用于自动化并且易于实现，但与此同时，它也有限制其证明和反驳它的能力。对于此解决方案，我们开发了一个强大的简化顺序，该顺序概括了称为加权路由顺序的简化顺序。该订单适合自动化，可以处理无法通过简化顺序证明的定理。（c）汇合是保证计算结果唯一性的属性，从而可以通过计算进行自动证明方程式证明。设计了一种技术来证明基于部分系统汇合的术语重写系统的汇合。在国际会议FSCD 2022上发表。