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回情報処理学会プログラミング研究発表会において報告した．

(equal equation payment) Unlimited number of rules for generating automatic counteractions Theorems for generating automatic counteractions Theorems on the basis of the basic theory of the law, the theory of the basic theory, the theory of the basic theory of the law, the theory of the basic theory, the theory of the theory, the theory of Non-environmental, non-basic environmental research. The specific results of this year are listed below. 1. A limited number of items are returned. There is no limit to the number of items. The basic performance index is not known. The performance is improved. The performance is limited. It is calculated that there is no limit to the performance of the machine. This is the result of important service cutting. In this study, the Japanese Academy of Sciences 39 returned to the General Assembly on the basis of the results of the decision. In this paper, we first study the proposal that there is no limit to the possibility of positive normalization of the program. Smullyan (1994) introduced the new protocol to combine the sub-protocol. 37 cases were successfully tested. The results showed that 31 cases were successful. 31 cases of ω-intensity were normalized, and the possibility that they were not detected was demonstrated. In combination, 37 cases were diagnosed as having a negative response, 32 cases were not environmentally friendly, 12 cases were terminative, non-obsolete, non-obsolete. There were 8 cases of non-basic clinical symptoms. In this study, the report will be reported in the 143rd case of the Institute of Science.

项目成果

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ページ

石见实验室网页