Journal and Conference Papers

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

• Yuki Sato and Takahito Aoto,
  Undecidability of some properties related to the uniqueness of normal forms for flat term rewiting systems(in Japanese),
  IPSJ Transactions on Programming, Vol.14, No.2, pp.15--24, 2021. [WEB]

• Kairi Miyamae and Takahito Aoto,
  A category-theoretic of formalization of unification over rational terms (in Japanese)
  IPSJ Transactions on Programming, 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]

• Yuta Kimura and Takahito Aoto,
  Formalizing Rewriting Induction on Isabelle/HOL (in Japanese)
  Computer Software, 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]

• Taichi Kurita and Takahito Aoto,
  Automated proofs of Horn-clause inductive theorems for conditional term rewriting systems
  Computer Sofware, 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]

• Kentaro Shimanuki, Takahito Aoto and Yoshihito Toyama
  Decision method of reachability based on rewrite rule overlapping (in Japanese)
  Computer Software, 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)]

• Koichi Sato, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama
  Automated inductive theorem proving using transformations of term rewriting systems (in Japanese)
  Computer Software, 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]

• Tatsunari Nakazima, Takahito Aoto and Yoshihito Toyama
  Decidability of inductive theorems based on rewriting induction (in Japanese)
  Computer Software, 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]

• Shota Takahashi, Takahito Aoto and Yoshihito Toyama
  Innermost reachability of bottom-up innermost term rewriting systems (in Japanese)
  Computer Software, 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]

• Tsubasa Suzuki, Takahito Aoto and Yoshihito Toyama
  Confluence proofs of term rewriting systems based on persistency (in Japanese)
  Computer Software, 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]

• Masaki Matoba, Takahito Aoto and Yoshihito Toyama
  Commutativity of term rewriting systems based on one side decreasing diagrams (in Japanese)
  Computer Software, 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

• Munehiro Iwami and Takahito Aoto
  Disproving strong head normalization and general productivity automatically in infinitary term rewriting systems (in japanese)
  Computer Software, Vol.29, No.1, pp.211-239, 2012. © JSSST
  [abstract] [web page (at J-STAGE)]

• Kouki Isobe, Takahito Aoto and Yoshihito Toyama
  A path ordering for term rewriting systems with polynomial size normal forms (in japanese)
  Computer Software, 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

• Junichi Yoshida, Takahito Aoto, Yoshihito Toyama
  Automating confluence check of term rewriting systems (in japanese)
  Computer Software, Vol.26, No.2, pp.76-92, 2009. © JSSST
  [abstract] [web page (at J-STAGE)]

• Satoshi Shimazu, Takahito Aoto, Yoshihito Toyama
  Automated lemma generation for rewriting induction with disproof (in japanese)
  Computer Software, 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]

• Junichi Yoshida, Takahito Aoto and Yoshihito Toyama
  Automating confluence check of term rewriting systems (in japanese)
  In Proceedings of the Forum on Information Technology 2007 (FIT2007), Information Technology Letters, 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)]

• Yuki Chiba, Takahito Aoto and Yoshihito Toyama
  Introducing sequence variables in program transformation based on templates (in japanese)
  In Proceedings of the Forum on Information Technology 2005 (FIT2005), Information Technology Letters, 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)]

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

• Takahito Aoto, Toshiyuki Yamada and Yoshihito Toyama
  Proving inductive theorems of higher-order functional programs (in japanese)
  In Proceedings of the Forum on Information Technology 2003 (FIT2003), Information Technology Letters, 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]

• Takahito Aoto and Toshiyuki Yamada
  Proving termination of simply typed term rewriting systems automatically (in japanese)
  IPSJ Transactions on Programming, Vol.44, No.SIG 4 (PRO 17), pp.67-77, 2003.
  [abstract] [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] [web page (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]

For research reports and other papers, please check here.