Automated Theorem Proving for Infinite Term Rewriting Systems

无限项重写系统的自动定理证明

• 批准号: 22K11904
• 负责人: 岩見 宗弘
• 金额: $ 2.66万
• 依托单位: Shimane University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2022
• 资助国家: 日本
• 起止时间: 2022-04-01 至 2025-03-31
• 项目状态: 未结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22K11904/
• 关键词: 項書き換えシステム; 無限項書き換えシステム; 正則項; 木変換器; 組合せ子; 非ω-強頭部正規化可能性; 非基礎ループ性; 非循環性; 無限項書換えシステム; 定理自動証明; 項書換えシステム

(等式付)無限項書換えシステムに対する生成性自動反証法および余帰納的定理自動証明法の基礎理論を構築することを目的として，正則項の木変換器による書き換えに関する研究を行った．さらに，組合せ子がもつ書き換え規則からなる項書き換えシステムの非ω-強頭部正規化可能性，非循環性，非基礎ループ性に関する研究を行った．本年度の具体的な成果は以下の通りである．1. 有限項の繰り返しから生じる無限項は正則項として知られており，基本的な性質に関する研究が進んでいる．正則項は，有限表現ができるため，計算機で扱える無限項として重要な役割を果たす．まず，決定性トップダウン木変換器を用いて，正則項を無限に書き換えてその極限として無限項が得られるならば，その無限項は正則項であることを証明した．また，この結果は，決定性マクロ木変換器に対しては成立しないことを反例をあげて示した．本研究は，日本ソフトウェア科学第39回大会において報告した．2. 先行研究で提案した無限項書き換えシステムに対するω-強頭部正規化可能性の反証手続きを，Smullyan(1994)により新しく紹介された組合せ子の書き換え規則からなる項書き換えシステム37例に対して適用した．その結果，31例について反証手続きが成功した．すなわち，31例がω-強頭部正規化可能性をもたないことを示した．また，組合せ子の書き換え規則からなる項書き換えシステム37例のうち32例が非循環性をもち，12例が停止性，非基礎ループ性と非ループ性をもつことを示した．さらに，2種類のラベル付け手法を提案し，8例が非基礎ループ性をもつことを示した．本研究は，第143回情報処理学会プログラミング研究発表会において報告した．

(Equation 2) Infinite term transformation of the theory of generative automatic proof and residual theorem automatic proof of the basic theory of the construction of the purpose, regular term transformation of the theory of the theory of transformation of the research. In this paper, the study of the relationship between the non-ω-strong head normalization possibility, non-cyclic property and non-basic property of the combination of sub-sets and the rule of transformation is carried out. This year's specific achievements are as follows: 1. The finite term returns to the infinite term and the regular term is known, and the research on the basic nature of the finite term is advancing. Regular term is finite expression, computer is infinite term is important cut fruit. The deterministic term is used to prove that the regular term is infinite and that the infinite term is infinite. The result is decisive. This study is a report to the 39th Japanese Science Conference. 2. Smullyan(1994) proposed a new approach to the study of the possibility of head normalization in the case of infinite term substitution, and proposed a new approach to the study of the possibility of head normalization in the case of 37 cases of head normalization. 31 cases were proved to be successful. 31 cases of ω-strong head normalization possibility. 37 cases are non-cyclic, 32 cases are non-cyclic, 12 cases are non-stop, non-basic and non-basic. In addition, 2 types of special treatment methods were proposed, and 8 cases of non-basic special treatment methods were proposed. This study is the 143rd report of the Information Processing Society.

项目成果

Rewriting of Rational Terms by Tree Transducer

用树换能器重写有理项

• 发表时间: 2022
• 作者: 鈴木月花;中垣好花;木村留美;北川雅恵;長嶺憲太郎;松本顕;Nozaki Takayuki;中村謙， 野崎隆之;中村謙， 野崎隆之;岩見宗弘;岩見宗弘;Munehiro Iwami;岩見宗弘;Munehiro Iwami
• 通讯作者: Munehiro Iwami

様々な組合せ子のω-強頭部正規化可能性の反証

反驳各种组合器的 ω-strong 头正则化性

• 发表时间: 2023
• 期刊: 第143回情報処理学会プログラミング研究会発表資料
• 作者: 鈴木月花;中垣好花;木村留美;北川雅恵;長嶺憲太郎;松本顕;Nozaki Takayuki;中村謙， 野崎隆之;中村謙， 野崎隆之;岩見宗弘
• 通讯作者: 岩見宗弘

正則項の木変換器による書き換え

使用树形转换器重写常规术语

• 发表时间: 2022
• 期刊: 日本ソフトウェア科学会第39回大会講演論文集
• 作者: 鈴木月花;中垣好花;木村留美;北川雅恵;長嶺憲太郎;松本顕;Nozaki Takayuki;中村謙， 野崎隆之;中村謙， 野崎隆之;岩見宗弘;岩見宗弘
• 通讯作者: 岩見宗弘

Rewriting of Rational Terms by Tree Transducer Revisited

重新审视树换能器对有理项的重写

• 发表时间: 2023
• 作者: 鈴木月花;中垣好花;木村留美;北川雅恵;長嶺憲太郎;松本顕;Nozaki Takayuki;中村謙， 野崎隆之;中村謙， 野崎隆之;岩見宗弘;岩見宗弘;Munehiro Iwami
• 通讯作者: Munehiro Iwami

岩見研究室webページ

石见实验室网页