研究課題
合流性(CR性)以外の解の一意性を保証する性質として，これまで研究されている性質には，正規形性(NFP性)，可換に関する一意正規形性(UNC性)，そして，簡約に関する一意正規形性(UNR性)の3つがある.これらの性質は，CR性⇒NFP性⇒UNC性⇒UNR性という論理関係がある.したがって，これらの3つの性質は合流性よりも弱い性質となっており，しかも，CR性，NFP性，UNC性，UNR性の順に階層を成している.本研究では，NFP性，UNC性，UNR性を始めとする，解の一意性を保証する，合流性より弱いさまざまな性質の検証理論や自動検証技術を開発する.最終年度では，UNR性を検証する手法について以下の成果が得られた．CR性とUNC性については，書き換え規則を追加または削除したときに，どのような場合に，それらの性質を保存するかという条件が知られている．同様の問題が，UNR性については知られていないことがわかり考察研究を進めた結果，UNR性についてのそのような条件を与えることができた．また，これらの条件について，UNR性のみならずUNC性も保存するが，CR性は保存しないことも明らかにし，UNR性の検証システムに用いる場合の扱い方に知見を与えた．さらに，UNC性がない場合のUNR性の検証方法には利用できないことも導かれる．そのため，UNC性を持たない場合のUNR性の検証方法が重要であることが明らかになり，その手法の考察研究を進め，2種類の手法を考案し，その正しさの証明を与えた．さらに，これらの検証手法の実装も行い，計算機実験によりその有効性を明らかにした．
すべて 2023
すべて 雑誌論文 (2件) (うち国際共著 1件、 査読あり 1件、 オープンアクセス 2件) 学会発表 (4件)
Proceedings of the 14th International Symposium on Frontiers of Combining Systems
巻: 14279 ページ: 99-116
10.1007/978-3-031-43369-6
Proceedings of the 12th International Workshop on Confluence
巻: NB ページ: 32-37
