発表論文
- Ryota Haga, Yuki Kagaya, and Takahito Aoto
A critical pair criterion for level-commutation of conditional term rewriting systems
In Proceedings of the 14th International Symposium on Frontiers of Combining Systems (FroCoS 2023), Czech, Czech Republic, September 20-22, pp.99-116, Lecture Notes in Artificial Intelligence, Vol.14279, Springer, 2023. © Springer-Verlag
[doi:10.1007/978-3-031-43369-6]
- Takahito Aoto, Nao Hirokawa, Dohan Kim, Misaki Kojima, Aart Middeldorp, Fabian
Mitterwallner, Naoki Nishida, Teppei Saito, Jonas Schöpf, Kiraku Shintani,
René Thiemann and Akihisa Yamada
A new format for rewrite systems,
In Proceedings of the 12th International Workshop on Confluence (IWC 2023), Obergurgl, Austria, August 2023, pp.32-37.
-
趙順, 青戸等人,
フラット右線形項書き換えシステムの簡約に関する一意正規形性の決定不能性,
第25回プログラミングおよびプログラミング言語ワークショップ(PPL 2023)論文集, 2023.
-
Ryota Haga, Yuki Kagaya, and Takahito Aoto,
A critical pair criterion for level-commutation of conditional term rewriting systems,
In Proceedings of the 11th International Workshop on Confluence (IWC 2022), pp.13-18, 2022.
-
望月美希, 青戸等人,
正則項書き換えにおける書き換えステップの決定可能性について,
日本ソフトウェア科学会第39回大会, 43-S, 2022.
[pdf]
-
趙順, 青戸等人,
フラット右線形項書き換えシステムの簡約に関する一意正規形性の決定不能性の証明について,
日本ソフトウェア科学会第39回大会, 42-S, 2022.
[pdf]
-
南山 駿人, 青戸 等人,
書き換え帰納法による帰納的定理証明と循環余帰納法による余帰納的定理証明の融合,
第24回プログラミングおよびプログラミング言語ワークショップ(PPL 2022)論文集, 2022.
-
芳賀 雅樹, 青戸 等人,
置換に関する不動点制約を用いた名目書き換え,
第24回プログラミングおよびプログラミング言語ワークショップ(PPL 2022)論文集, 2022.
-
大野 峻, 青戸 等人,
交差式条件付き項書き換えシステムに対するアンラベリング変換の健全性について,
第24回プログラミングおよびプログラミング言語ワークショップ(PPL 2022)論文集, 2022.
-
芳賀 亮太, 青戸 等人,
危険対条件に基づく条件付き項書き換えシステムの階層可換性,
第24回プログラミングおよびプログラミング言語ワークショップ(PPL 2022)論文集, 2022.
-
Kentaro Kikuchi, Takahito Aoto,
Simple derivation systems for proving sufficient completeness of non-terminating term rewriting systems,
In Proceedings of the 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021), Virtual Event, December 15-17, pp.49:1-49:15, Leibniz International Proceedings in Informatics, Vol.213, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2021.
[doi:10.4230/LIPIcs.FSTTCS.2021.49] -
Tomoki Shiraishi, Kentaro Kikuchi and Takahito Aoto,
A proof method for local sufficient completeness of term rewriting systems,
In Proceedings of the 18th International International Colloquium on Theoretical Aspects of Computing (ICTAC 2021), Virtual Event, Nur-Sultan, Kazakhstan, September 8-10, pp.386-404, Lecture Notes in Computer Science, Vol.12819, Springer, 2021.
[doi:10.1007/978-3-030-85315-0] -
芳賀亮太, 青戸等人,
危険対条件に基づく条件付き項書き換えシステムの階層可換性,
日本ソフトウェア科学会第38回大会, 41-L, 2021.
[pdf] -
佐藤 悠稀 , 青戸 等人,
フラット項書き換えシステムにおける正規形の一意性に関する性質の決定不能性,
情報処理学会論文誌プログラミング（PRO）, Vol.14, No.2, pp.15--24, 2021. [WEB] -
宮前 海里, 青戸 等人,
圏論に基づく正則項上の単一化の形式化,
情報処理学会論文誌プログラミング（PRO）,Vol.14, No.2, pp.1--14, 2021. [WEB] -
Mamoru Ishizuka, Takahito Aoto and Munehiro Iwami,
Commutative rational term rewriting,
In Proceedings of the 15th International Conference on Language and Automata Theory and Applications (LATA 2021), Milan, Italy, March 2021, pp.200-212, Lecture Notes in Computer Science, Vol.12638 Springer-Verlag. © Springer-Verlag
[doi:10.1007/978-3-030-68195-1] -
Kentaro Kikuchi and Takahito Aoto,
Confluence and commutation for nominal rewriting systems with atom-variables,
In Proceedings of the 30th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2020), Bologna, Italy, September 7-9,pp.56-73, Lecture Notes in Computer Science, Vol.12561, Springer, 2020.
[doi:10.1007/978-3-030-68446-4_3] -
Masaomi Yamaguchi and Takahito Aoto,
A fast decision procedure for uniqueness of normal forms w.r.t. conversion of shallow term rewriting systems,
In Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Paris, France, July 2020, pp.11:1-11:23, Leibniz International Proceedings in Informatics, Vol.167, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2020.
[doi:10.4230/LIPIcs.FSCD.2020.11] -
木村 優太, 青戸 等人,
対話的定理証明器Isabelle/HOL上での書き換え帰納法の形式化,
コンピュータソフトウェア, Vol.37, No.2, pp.104-119, 2020. © JSSST
[doi:10.11309/jssst.37.2_104] - 石塚守, 青戸等人, 岩見宗弘,
交換律による正則項書き換えにおける有限オートマトンの構成法とその応用,
第22回プログラミングおよびプログラミング言語ワークショップ(PPL 2020)論文集, 2020.
- 加賀谷有輝, 青戸等人,
条件付き項書き換えシステムの階層合流性証明法,
第22回プログラミングおよびプログラミング言語ワークショップ(PPL 2020)論文集, 2020.
- 白石智輝, 青戸等人, 菊池健太郎,
項書き換えシステムにおける局所十分完全性の証明法,
第22回プログラミングおよびプログラミング言語ワークショップ(PPL 2020)論文集, 2020.
-
Kentaro Kikuchi, Takahito Aoto and Isao Sasano,
Inductive theorem proving in non-terminating rewriting systems and its application to program transformation,
In Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming (PPDP 2019), Porto, Portugal, October 2019, pp.13:1-13:14, ACM Press.
[doi:10.1145/3354166.3354178] -
Takahito Aoto and Yoshihito Toyama,
Automated proofs of unique normal forms w.r.t. conversion for term rewriting systems,
In Proceedings of the 12th International Symposium on Frontiers of Combining Systems (FroCoS 2019), London, UK, September 2019, pp.330-347, Lecture Notes in Artificial Intelligence, Vol.11715, Springer-Verlag. © Springer-Verlag
[doi:10.1007/978-3-030-29007-8_19] -
栗田泰智, 青戸等人,
条件付き項書き換えシステムにおけるホーン節帰納的定理の自動証明,
コンピュータソフトウェア, Vol.36, No.2, pp.61-75, 2019. © JSSST
[doi:10.11309/jssst.36.2_61] - 山口諒, 青戸等人,
決定手続きを用いた項書き換えシステムの帰納的定理自動証明,
第21回プログラミングおよびプログラミング言語ワークショップ(PPL 2019)論文集, 2019.
- 加藤裕人, 青戸等人,
書き換え帰納法を利用した帰納的定理証明の補題生成法,
第21回プログラミングおよびプログラミング言語ワークショップ(PPL 2019)論文集, 2019.
-
石塚守, 青戸等人,
Jaffarのアルゴリズムに基づく正則項の単一化,
日本ソフトウェア科学会第35回大会, PPL3-4-S, 2018.
[pdf] -
山口諒, 青戸等人,
決定手続きを用いた項書き換えシステムの帰納的定理自動証明,
日本ソフトウェア科学会第35回大会, PPL2-3-S, 2018.
[pdf] -
Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani and Harald Zankl,
Confluence Competition 2018,
In Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Oxford, UK, July 2018, pp.32:1-32:5, Leibniz International Proceedings in Informatics, Vol.108, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2018. [doi:10.4230/LIPIcs.FSCD.2018.32] - Takahito Aoto and Yoshihito Toyama,
Automated proofs of unique normal forms w.r.t. conversion for term rewriting systems,
CoRR abs/1807.00940, 2018. - 栗田泰智, 青戸等人,
条件付き項書き換えシステムにおけるホーン節帰納的定理の自動証明,
第20回プログラミングおよびプログラミング言語ワークショップ(PPL 2018)論文集, 2018.
-
Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama,
Parallel closure theorem for left-linear nominal rewriting systems,
In Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017), Brasília, Brazil, September 2017, pp.115-131, Lecture Notes in Computer Science, Vol.10483, Springer-Verlag. © Springer-Verlag
[doi:10.1007/978-3-319-66167-4_7] -
加藤裕人, 青戸等人,
書き換え帰納法を利用した帰納的定理証明の補題生成法,
日本ソフトウェア科学会第34回大会, PPL4-1, 2017.
[pdf] -
萩原崇央, 青戸等人,
極大完備化に基づく等式定理の自動証明,
日本ソフトウェア科学会第34回大会, PPL2-1, 2017.
[pdf] -
Takahito Aoto, Yoshihito Toyama and Yuta Kimura,
Improving rewriting induction approach for proving ground confluence,
In Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Oxford, UK, 2017, pp.7:1-7:18, Leibniz International Proceedings in Informatics, Vol.84, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
[doi:10.4230/LIPIcs.FSCD.2017.7] -
島貫健太郎, 青戸等人, 外山 芳人,
書き換え規則の重なりに基づく到達可能性判定法,
コンピュータソフトウェア, Vol.33, No.3, pp.93-107, 2016. © JSSST
[doi:10.11309/jssst.33.3_93] -
Takahito Aoto and Kentaro Kikuchi,
Nominal confluence tool,
In Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR 2016), Coimbra, Portugal, 2016, pp.173-182, Lecture Notes in Computer Science, Vol.9706, Springer-Verlag. © Springer-Verlag
[doi:10.1007/978-3-319-40229-1_12] -
Takahito Aoto and Yoshihito Toyama,
Ground confluence prover based on rewriting induction,
In Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Porto, Portugal, 2016, pp.33:1-33:12, Leibniz International Proceedings in Informatics, Vol.52, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
[doi:10.4230/LIPIcs.FSCD.2016.33] -
Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama,
Critical pair analysis in nominal rewriting,
In Proceedings of the 7th International Symposium on Symbolic Computation in Software Science (SCSS 2016), Tokyo, Japan, March, 2016, pp.156-168, EPiC Series in Computing, Vol.39, EasyChair.
[web page (at EasyChair)]