ジャーナル論文，国際会議論文

• 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]
  

• 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. © Springer-Verlag
  [doi:10.1007/978-3-030-85315-0]

• 佐藤 悠稀 , 青戸 等人,
  フラット項書き換えシステムにおける正規形の一意性に関する性質の決定不能性,
  情報処理学会論文誌プログラミング（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 Sy nthesis 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]

• 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.
  [abstract] [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
  [abstract] [pdf, full version, 26 pages] [doi:10.1007/978-3-030-29007-8_19]

• 栗田泰智, 青戸等人
  条件付き項書き換えシステムにおけるホーン節帰納的定理の自動証明
  コンピュータソフトウェア, Vol.36, No.2, pp.61-75, 2019. © JSSST
  [abstract] [doi:10.11309/jssst.36.2_61]

• 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.
  [abstract] [doi:10.4230/LIPIcs.FSCD.2018.32]

• 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
  [abstract] [pdf, 17 pages] [doi:10.1007/978-3-319-66167-4_7]

• 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.
  [abstract] [pdf, 18 pages] [doi:10.4230/LIPIcs.FSCD.2017.7]

• 島貫健太郎, 青戸等人, 外山 芳人
  書き換え規則の重なりに基づく到達可能性判定法
  コンピュータソフトウェア, Vol.33, No.3, pp.93-107, 2016. © JSSST
  [abstract] [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, June-July 2016, pp.173-182, Lecture Notes in Computer Science, Vol.9706, Springer-Verlag. © Springer-Verlag
  [abstract] [pdf, 9 pages] [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, June 2016, pp.33:1-33:12, Leibniz International Proceedings in Informatics, Vol.52, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  [abstract] [pdf, 12 pages] [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.
  [abstract] [pdf, 13 pages] [web page (at EasyChair)]

• Koichi Sato, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama
  Correctness of context-moving transformations for term rewriting systems
  In Proceedings of 25th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2015), Siena, Italy, July 2015, pp.331-345, Lecture Notes in Computer Science, Vol.9527, Springer-Verlag. © Springer-Verlag
  [abstract] [pdf, 15 pages] [doi:10.1007/978-3-319-27436-2_20]

• Takahito Aoto, Nao Hirokawa, Julian Nagele, Naoki Nishida and Harald Zankl
  Confluence Competition 2015
  In Proceedings of the 25th International Conference on Automated Deduction (CADE-25), Berlin, Germany, August 2015, pp.101-104.
  [abstract] [pdf, 4 pages]

• Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama
  Confluence of orthogonal nominal rewriting systems revisited
  In Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015), Warsaw, Poland, June-July 2015, pp.301-317, Leibniz International Proceedings in Informatics, Vol.36, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  [abstract] [pdf, 15 pages] [doi:10.4230/LIPIcs.RTA.2015.301] [web page (at Dagstuhl)]

• 佐藤洸一, 菊池健太郎, 青戸等人, 外山 芳人
  項書き換えシステムの変換を利用した帰納的定理自動証明
  コンピュータソフトウェア, Vol.32, No.1, pp.179-193, 2015. © JSSST
  [abstract] [doi:10.11309/jssst.32.1_179]

• Takahito Aoto and Sorin Stratulat
  Decision procedures for proving inductive theorems without induction
  In Proceedings of 16th International Symposium on Principles and Practice of Declarative Programming (PPDP 2014), Canterbury, UK, September 2014, pp.237-248, ACM Press.
  [abstract] [pdf, 11 pages] [doi:10.1145/2643135.2643156]

• 中嶋辰成, 青戸等人, 外山芳人
  書き換え帰納法に基づく帰納的定理の決定可能性
  コンピュータソフトウェア, Vol.31, No.3, pp.294-306, 2014. © JSSST
  [abstract] [doi:10.11309/jssst.31.3_294]

• Takahito Aoto, Yoshihito Toyama and Kazumasa Uchida
  Proving confluence of term rewriting systems via persistency and decreasing diagrams
  In Proceedings of Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014), Vienna, Austria, July 2014, pp.46-60, Lecture Notes in Computer Science, Vol.8560, Springer-Verlag. © Springer-Verlag
  [abstract] [pdf, 15 pages] [doi:10.1007/978-3-319-08918-8_4]

• 高橋翔大, 青戸等人, 外山芳人
  ボトムアップ最内項書き換えシステムの最内到達可能性
  コンピュータソフトウェア, Vol.31, No.1, pp.75-89, 2014. © JSSST
  [abstract] [doi:10.11309/jssst.31.1_75]

• Takahito Aoto
  Disproving confluence of term rewriting systems by interpretation and ordering
  In Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), Nancy, France, September 2013, pp.311-326, Lecture Notes in Artificial Intelligence, Vol.8152, Springer-Verlag. © Springer-Verlag
  [abstract] [pdf, 16 pages] [doi:10.1007/978-3-642-40885-4_22]

• 鈴木翼, 青戸等人, 外山芳人
  永続性に基づく項書き換えシステムの合流性証明法
  コンピュータソフトウェア, Vol.30, No.3, pp.148-162, 2013. © JSSST
  [abstract] [doi:10.11309/jssst.30.3_148]

• Takahito Aoto and Munehiro Iwami
  Termination of rule-based calculi for uniform semi-unification
  In Proceedings of the 7th International Conference on Language and Automata Theory and Applications (LATA 2013), Bilbao, Spain, April 2013, pp.56-67, Lecture Notes in Computer Science, Vol.7810, Springer-Verlag. © Springer-Verlag
  [abstract] [pdf, 12 pages] [doi:10.1007/978-3-642-37064-9_7]

• 的場正樹, 青戸等人, 外山芳人
  片側減少ダイアグラム法による項書き換えシステムの可換性証明法
  コンピュータソフトウェア, Vol.30, No.1, pp.187-202, 2013. © JSSST
  [abstract] [doi:10.11309/jssst.30.1_187]

• Takahito Aoto and Jeroen Ketema
  Rational term rewriting revisited: decidability and confluence
  In Proceedings of the 6th International Conference on Graph Transformation (ICGT 2012), Bremen, Germany, September 2012, pp.172-186, Lecture Notes in Computer Science, Vol.7562, Springer-Verlag. © Springer-Verlag
  [abstract] [pdf, 15 pages] [doi:10.1007/978-3-642-33654-6_12] [web page (at Springer)]

• Takahito Aoto and Yoshihito Toyama
  A reduction-preserving completion for proving confluence of non-terminating term rewriting systems
  Logical Methods in Computer Science, Vol.8, No.1:31, pp.1-29, 2012.
  [abstract] [web page (at LMCS)] experiments

• 岩見宗弘, 青戸等人
  無限項書き換えシステムにおける強頭部正規化可能性および一般生成性の自動反証
  コンピュータソフトウェア, Vol.29, No.1, pp.211-239, 2012. © JSSST
  [abstract] [web page (at J-STAGE)]

• 磯部耕己, 青戸等人, 外山芳人
  多項式サイズ正規形を保証する項書き換えシステムの経路順序
  コンピュータソフトウェア, Vol.29, No.1, pp.176-190, 2012. © JSSST
  [abstract] [web page (at J-STAGE)]

• Takahito Aoto, Toshiyuki Yamada and Yuki Chiba
  Natural inductive theorems for higher-order rewriting
  In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), Novi Sad, Serbia, May/June 2011, pp.107-121, Leibniz International Proceedings in Informatics, Vol.10, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  [abstract] [pdf, 15 pages] [web page (at Dagstuhl)]

• Takahito Aoto and Yoshihito Toyama
  Reduction-preserving completion for proving confluence of non-terminating term rewriting systems
  In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), Novi Sad, Serbia, May/June 2011, pp.91-106, Leibniz International Proceedings in Informatics, Vol.10, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  [abstract] [pdf, 16 pages] [web page (at Dagstuhl)] experiments

• Takahito Aoto
  Automated confluence proof by decreasing diagrams based on rule-labelling
  In Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), Edingburgh, UK, July 2010, pp.7-16, Leibniz International Proceedings in Informatics, Vol.6, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  [abstract] [pdf, 10 pages] [web page (at Dagstuhl)] experiments

• Yuki Chiba, Takahito Aoto and Yoshihito Toyama
  Program transformation templates for tupling based on term rewriting
  IEICE Transactions on Information and Systems, Vol.E93-D, No.5, pp.963-973, 2010.
  [abstract] [web page (at IEICE)]

• Takahito Aoto and Toshiyuki Yamada
  Argument filterings and usable rules for simply typed dependency pairs
  In Proceedings of the 7th International Symposium on Frontiers of Combining Systems (FroCoS 2009), Trento, Italy, September 2009, pp.117-132, Lecture Notes in Artificial Intelligence, Vol.5749, Springer-Verlag. © Springer-Verlag
  [abstract] [pdf, 15 pages] [web page (at Springer)]

• Takahito Aoto, Junichi Yoshida and Yoshihito Toyama
  Proving confluence of term rewriting systems automatically
  In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009), Brasília, Brazil, June/July 2009, pp.93-102, Lecture Notes in Computer Science, Vol.5595, Springer-Verlag. © Springer-Verlag
  [abstract] [pdf, 10 pages] [web page (at Springer)] experiments ACP web page

• 吉田順一, 青戸等人, 外山芳人
  項書き換えシステムの合流性自動判定
  コンピュータソフトウェア, Vol.26, No.2, pp.76-92, 2009. © JSSST
  [abstract] [web page (at J-STAGE)]

• 嶌津聡志, 青戸等人, 外山芳人
  反証機能付き書き換え帰納法のための補題自動生成法
  コンピュータソフトウェア, Vol.26, No.2, pp.41-55, 2009. © JSSST
  [abstract] [web page (at J-STAGE)]

• Takahito Aoto
  Sound lemma generation for proving inductive validity of equations
  In Proceedings of the 28th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008), Bangalore, India, December 2008, pp.13--24, Leibniz International Proceedings in Informatics, Vol.2, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
  [abstract] [pdf, 15 pages] [web page (at Dagstuhl)]

• Takahito Aoto
  Soundness of rewriting induction based on an abstract principle
  IPSJ Transactions on Programming, Vol.49, No.SIG 1 (PRO 35), pp.28-38, 2008.
  [abstract] [pdf, 11 pages]

• Yuki Chiba, Takahito Aoto and Yoshihito Toyama
  Automatic construction of program transformation templates
  IPSJ Transactions on Programming, Vol.49, No.SIG 1 (PRO 35), pp.14-27, 2008.
  [abstract] [pdf, 14 pages]

• 吉田順一, 青戸等人, 外山芳人
  項書き換えシステムの合流性自動判定
  第6回情報科学技術フォーラム(FIT2007)講演論文集, 情報技術レターズ, Vol.6, pp.31-34, 2007.
  [pdf, 4 pages]

• Yuki Chiba, Takahito Aoto and Yoshihito Toyama
  Program transformation by templates: A rewriting framework
  IPSJ Transactions on Programming, Vol.47, No.SIG 16 (PRO 31), pp.52-65, 2006.
  [abstract] [pdf, 15 pages]

• Yuki Chiba and Takahito Aoto
  RAPT: A program transformation system based on term rewriting
  In Proceedings of the 17th International Conference on Rewriting Techniques and Applications (RTA 2006), Seattle, WA, USA, August 2006, pp.267-276, Lecture Notes in Computer Science, Vol.4098, Springer-Verlag. © Springer-Verlag
  [abstract] [pdf, 10 pages] [ps, 10 pages] [web page (at Springer)]

• Takahito Aoto
  Dealing with non-orientable equations in rewriting induction
  In Proceedings of the 17th International Conference on Rewriting Techniques and Applications (RTA 2006), Seattle, WA, USA, August 2006, pp.242-256, Lecture Notes in Computer Science, Vol.4098, Springer-Verlag. © Springer-Verlag
  [abstract] [pdf, 15 pages] [ps, 15 pages] [web page (at Springer)]

• 千葉勇輝, 青戸等人, 外山芳人
  パターンに基づくプログラム変換における列変数の導入
  第4回情報科学技術フォーラム(FIT2005)講演論文集, 情報技術レターズ, Vol.4, pp.5-8, 2005.
  [pdf, 4 pages]

• Yuki Chiba, Takahito Aoto and Yoshihito Toyama
  Program transformation by templates based on term rewriting
  In Proceedings of the 7th ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP'05), Lisbon, Portugal, July 2005, pp.59-69, ACM Press.
  [abstract] [ps, 11 pages]

• Takahito Aoto and Toshiyuki Yamada
  Dependency pairs for simply typed term rewriting
  In Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA 2005), Nara, Japan, April 2005, pp.120-134, Lecture Notes in Computer Science, Vol.3467, Springer-Verlag. © Springer-Verlag
  [abstract] [ps, 15 pages] [web page (at Springer)] [sttrs-examples-050508.tgz]

• Takahito Aoto, Toshiyuki Yamada and Yoshihito Toyama
  Inductive theorems for higher-order rewriting
  In Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA 2004), Aachen, Germany, June 2004, pp.269-284, Lecture Notes in Computer Science, Vol.3091, Springer-Verlag. © Springer-Verlag
  [abstract] [ps, 16 pages]

• 青戸等人, 山田俊行, 外山芳人
  高階関数型プログラムにおける帰納的定理証明
  第2回情報科学技術フォーラム(FIT2003)講演論文集, 情報技術レターズ, Vol.2, pp.21-22, 2003.
  [pdf, 2 pages]

• Takahito Aoto and Toshiyuki Yamada
  Termination of simply typed term rewriting systems by translation and labelling
  In Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA'03), Valencia, Spain, June 2003, pp.380-394, Lecture Notes in Computer Science, Vol.2706, Springer-Verlag. © Springer-Verlag
  [abstract] [ps, 15 pages]

• 青戸等人, 山田俊行
  単純型付き項書換え系における停止性の自動証明
  情報処理学会論文誌：プログラミング, Vol.44, No.SIG 4 (PRO 17), pp.67-77, 2003.
  [概要] [ps, 11 pages]

• Takahito Aoto
  Solution to the problem of Zantema on a persistent property of term rewriting systems
  Journal of Functional and Logic Programming, Vol.2001, No.11, 2001.
  [abstract] [http (at JFLP)]

• Takahito Aoto and Hiroyuki Shirasu
  On the finite model property of intuitionistic modal logics over MIPC
  Mathematical Logic Quarterly, Vol.45, No.4, pp.435-448, 1999.
  [abstract]

• Takahito Aoto
  Uniqueness of normal proofs in implicational intuitionistic logic
  Journal of Logic, Language and Information, Vol.8, No.2, pp.217-242, 1999.
  [abstract]

• Takahito Aoto
  Solution to the problem of Zantema on a persistent property of term rewriting systems
  In Proceedings of the Joint International Symposium PLILP/ALP'98, Pisa, Italy, September 1998, pp.250-265, Lecture Notes in Computer Science, Vol.1490, Springer-Verlag. © Springer-Verlag
  [abstract] [ps, 16 pages]

• Takahito Aoto and Yoshihito Toyama
  Termination transformation by tree lifiting ordering
  In Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98), Tsukuba, Japan, March/April 1998, pp.256-270, Lecture Notes in Computer Science, Vol.1379, Springer-Verlag. © Springer-Verlag
  [abstract] [ps, 15 pages]

• Takahito Aoto and Yoshihito Toyama
  On composable properties of term rewriting systems
  In Proceedings of the 6th International Conference on Algebraic and Logic Programming (ALP'97), Southampton, UK, September 1997, pp.114-128, Lecture Notes in Computer Science, Vol.1298, Springer-Verlag. © Springer-Verlag
  [abstract] [ps, 15 pages]

• Takahito Aoto and Yoshihito Toyama
  Persistency of confluence
  Journal of Universal Computer Science, Vol.3, No.11, pp.1134-1147, 1997.
  [abstract] [http (at JUCS)]

• Takahito Aoto and Hiroakira Ono
  Non-uniqueness of normal proofs for minimal formulas in implication-conjunction fragment of BCK
  Bulletin of the Section of Logic, Vol.23, No.3, pp.104-112, 1994.
  [abstract] [ps, 9 pages]