Core Concepts
等式述語、コンテキストリライティング、バリアントベースの簡略化を組み合わせた新しい帰納的推論システムを提案する。このシステムは、ユーザーの介入を必要とする9つのルールと、自動化できる11のルールから構成される。これにより、証明の大部分を自動化できる。
Abstract
本論文は、等式述語、狭義化、コンストラクタバリアントユニフィケーション、バリアントの充足可能性、順序付きコングルエンスクロージャ、コンテキストリライティング、順序付きリライティング、再帰的パス順序などの高度な等式推論技術を組み合わせた新しい帰納的推論システムを提案している。これらの技術はすべて、結合性、可換性、単位元の任意の組み合わせのアキシオムBの下で動作する。これらの推論ルールの多くは、Maude's NuITPの帰納的定理証明器に既に実装されている。
提案するシステムは、ユーザーの介入を必要とする9つのルールと、自動化できる11のルールから構成される。これにより、証明の大部分を自動化できる。自動化ルールは単独でも部分的な答えを出すことができる強力な簡略化ルールである。例えば、NuITPプローバーに実装されたルールは、DM-Checkツールが無限状態システムの不変式を証明する際に生成される検証条件を自動的に証明するために呼び出されている。
この推論システムの有効性は、これらの自動化ルールの新しい組み合わせによるものと考えられる。これらの技術の多くは既知のものであり、一部は自動一階定理証明器で広く使われているが、ここでは帰納的定理証明の目的で前例のないほど広範囲かつ一般的に組み合わせられている。
Stats
提案するシステムには20の推論ルールがあり、そのうち9つはユーザーの介入を必要とする。残りの11ルールは自動化できる。
自動化ルールは単独でも部分的な答えを出すことができる強力な簡略化ルールである。
NuITPプローバーに実装されたルールは、DM-Checkツールが生成する検証条件を自動的に証明するために使われている。