書き換え帰納法による帰納的定理証明と循環余帰納法による余帰納的定理証明の融合

• Item type: Trans(1)
• 公開日: 2022-05-20
• タイトル: 書き換え帰納法による帰納的定理証明と循環余帰納法による余帰納的定理証明の融合
• タイトル / 言語: en
• タイトル: Fusion of Inductive Theorem Proving Based on Rewriting Induction and Coinductive Theorem Proving Based on Circular Coinduction
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [発表概要, Unrefereed Presentatin Abstract]
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 新潟大学自然科学研究科
• 著者所属: 新潟大学自然科学研究科
• 著者所属(英): en
• 著者所属(英): Granduate School of Science and Technology, Niigata University
• 著者所属(英): en
• 著者所属(英): Granduate School of Science and Technology, Niigata University
• 著者名: 南山, 駿人; 青戸, 等人
• 著者名(英): Hayato, Minamiyama; Takahito, Aoto
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 等式論理において，自然数やリストなどの帰納的なデータ構造上で成立する等式を帰納的定理とよぶ．また，ストリームや無限木などの余帰納的なデータ構造上で成立する等式を余帰納的定理とよぶ．そして，項書き換えシステムに基づく帰納的定理の自動証明法として，書き換え帰納法(Reddy, 1990)が知られており，余帰納的定理の自動証明手法としては，循環余帰納法(Grigore Roşu & Dorel Lucanu, 2014)が知られている．一方，自然数のストリームなど，帰納的なデータ構造と余帰納的なデータ構造が混合したデータ構造に対しては，帰納的定理証明と余帰納的定理証明を同時に行う必要があると考えられるが，そのような自動証明法は従来あまり提案されていない．本発表では，書き換え帰納法と循環余帰納法を融合した証明体系を提案する．書き換え帰納法も循環余帰納法も等式集合と書き換え規則集合の対に対する導出体系として与えられているため，両者の導出規則を合併することは容易である．しかし，融合した証明体系で導出が成功したとしても，それぞれの導出規則のみで導出されているわけではない．このため，導出に成功した等式がどのような場合に帰納的定理や余帰納的定理となるかは自明ではない．提案手法を用いることにより，帰納的なデータ構造と余帰納的なデータ構造が組み合わさった場合にも，書き換え帰納法と循環余帰納法に基づく自動証明が可能となる．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In equational logic, equations valid on inductive data structures such as natural numbers or lists are called inductive theorems, and those valid on coinductive data structures such as streams and infinite trees are called coinductive theorems. To prove inductive theorems and coinductive theorems automatically, several methods have been proposedーone of such methods for proving inductive theorems is rewriting induction (Reddy, 1990), and one of such for proving coinductive theorem is circular coinduction (Grigore Roşu and Dorel Lucanu, 2014). There can be also data structures in which inductive and coinductive data structures are mixed, e.g., streams of natural numbersーfor proving properties of such data structures, it seems necessary to carry out inductive theorem proving and coinductive theorem proving simultaneously. Contrast to the methods for inductive/coinductive theorems proving, however, automated methods capable of dealing such mixed data structures have not been well-known previously. In this presentation, we propose a proof system that combines the rewriting induction and the circular coinduction. Since both the rewriting induction and the circular coinduction are given as derivation systems for pairs of a set of equations and a set of rewrite rules, it is easy to merge the derivation rules of both methods. However, even if the derivation succeeds in the combined proof system, the derivation may contains derivation steps from both of the systems, and thus it is not at all obvious that, under which situation, the equations with a successful derivation are inductively/coinductively valid. The proposed method is capable of proving inductive theorems and coinductive theorems for the mixed data structures automatically, using derivation rules of the rewriting induction and the circular coinduction.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 15, 号 2, p. 6-6, 発行日 2022-05-20
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会