On Composable Properties of Term Rewriting Systems. - Takahito Aoto 001; Yoshihito Toyama (ALP/HOA, 1997)

Persistency of Confluence. - Takahito Aoto 001; Yoshihito Toyama (J. Univers. Comput. Sci., 1997)

Termination Transformation by Tree Lifting Ordering. - Takahito Aoto 001; Yoshihito Toyama (RTA, 1998)

Uniqueness of Normal Proofs in Implicational Intuitionistic Logic. - Takahito Aoto 001 (J. Log. Lang. Inf., 1999)

On the Finite Model Property of Intuitionistic Modal Logics over MIPC. - Takahito Aoto 001; Hiroyuki Shirasu (Math. Log. Q., 1999)

Solution to the Problem of Zantema on a Persistent Property of Term Rewriting Systems. - Takahito Aoto 001 (J. Funct. Log. Program., 2001)

Termination of Simply Typed Term Rewriting by Translation and Labelling. - Takahito Aoto 001; Toshiyuki Yamada (RTA, 2003)

Inductive Theorems for Higher-Order Rewriting. - Takahito Aoto 001; Toshiyuki Yamada; Yoshihito Toyama (RTA, 2004)

Program transformation by templates based on term rewriting. - Yuki Chiba; Takahito Aoto 001; Yoshihito Toyama (PPDP, 2005)

Dependency Pairs for Simply Typed Term Rewriting. - Takahito Aoto 001; Toshiyuki Yamada (RTA, 2005)

Dealing with Non-orientable Equations in Rewriting Induction. - Takahito Aoto 001 (RTA, 2006)

RAPT: A Program Transformation System Based on Term Rewriting. - Yuki Chiba; Takahito Aoto 001 (RTA, 2006)

Program Transformation by Templates: A Rewriting Framework. - Yuki Chiba; Takahito Aoto 001; Yoshihito Toyama (Inf. Media Technol., 2007)

Sound Lemma Generation for Proving Inductive Validity of Equations. - Takahito Aoto 001 (FSTTCS, 2008)

Soundness of Rewriting Induction Based on an Abstract Principle. - Takahito Aoto 001 (Inf. Media Technol., 2008)

Automatic Construction of Program Transformation Templates. - Yuki Chiba; Takahito Aoto 001; Yoshihito Toyama (Inf. Media Technol., 2008)

Argument Filterings and Usable Rules for Simply Typed Dependency Pairs. - Takahito Aoto 001; Toshiyuki Yamada (FroCoS, 2009)

Proving Confluence of Term Rewriting Systems Automatically. - Takahito Aoto 001; Junichi Yoshida; Yoshihito Toyama (RTA, 2009)

Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling. - Takahito Aoto 001 (RTA, 2010)

Program Transformation Templates for Tupling Based on Term Rewriting. - Yuki Chiba; Takahito Aoto 001; Yoshihito Toyama (IEICE Trans. Inf. Syst., 2010)

Natural Inductive Theorems for Higher-Order Rewriting. - Takahito Aoto 001; Toshiyuki Yamada; Yuki Chiba (RTA, 2011)

Rational Term Rewriting Revisited: Decidability and Confluence. - Takahito Aoto 001; Jeroen Ketema (ICGT, 2012)

A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems - Takahito Aoto 001; Yoshihito Toyama (Log. Methods Comput. Sci., 2012)

Preface. - Takahito Aoto 001; Aart Middeldorp (Theor. Comput. Sci., 2012)

Disproving Confluence of Term Rewriting Systems by Interpretation and Ordering. - Takahito Aoto 001 (FroCos, 2013)

Termination of Rule-Based Calculi for Uniform Semi-Unification. - Takahito Aoto 001; Munehiro Iwami (LATA, 2013)

Decision Procedures for Proving Inductive Theorems without Induction. - Takahito Aoto 001; Sorin Stratulat (PPDP, 2014)

Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams. - Takahito Aoto 001; Yoshihito Toyama; Kazumasa Uchida (RTA-TLCA, 2014)

Confluence Competition 2015. - Takahito Aoto 001; Nao Hirokawa; Julian Nagele; Naoki Nishida 001; Harald Zankl (CADE, 2015)

Correctness of Context-Moving Transformations for Term Rewriting Systems. - Koichi Sato; Kentaro Kikuchi; Takahito Aoto 001; Yoshihito Toyama (LOPSTR, 2015)

Confluence of Orthogonal Nominal Rewriting Systems Revisited. - Takaki Suzuki; Kentaro Kikuchi; Takahito Aoto 001; Yoshihito Toyama (RTA, 2015)

Nominal Confluence Tool. - Takahito Aoto 001; Kentaro Kikuchi (IJCAR, 2016)

Ground Confluence Prover based on Rewriting Induction. - Takahito Aoto 001; Yoshihito Toyama (FSCD, 2016)

Critical Pair Analysis in Nominal Rewriting. - Takaki Suzuki; Kentaro Kikuchi; Takahito Aoto 001; Yoshihito Toyama (SCSS, 2016)

Parallel Closure Theorem for Left-Linear Nominal Rewriting Systems. - Kentaro Kikuchi; Takahito Aoto 001; Yoshihito Toyama (FroCoS, 2017)

Improving Rewriting Induction Approach for Proving Ground Confluence. - Takahito Aoto 001; Yoshihito Toyama; Yuta Kimura (FSCD, 2017)

Confluence Competition 2018. - Takahito Aoto 001; Makoto Hamana; Nao Hirokawa; Aart Middeldorp; Julian Nagele; Naoki Nishida 001; Kiraku Shintani; Harald Zankl (FSCD, 2018)

Automated Proofs of Unique Normal Forms w.r.t. Conversion for Term Rewriting Systems. - Takahito Aoto 001; Yoshihito Toyama (FroCos, 2019)

Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation. - Kentaro Kikuchi; Takahito Aoto 001; Isao Sasano (PPDP, 2019)

A Fast Decision Procedure For Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting Systems. - Masaomi Yamaguchi; Takahito Aoto 001 (FSCD, 2020)

Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables. - Kentaro Kikuchi; Takahito Aoto 001 (LOPSTR, 2020)

Simple Derivation Systems for Proving Sufficient Completeness of Non-Terminating Term Rewriting Systems. - Kentaro Kikuchi; Takahito Aoto 001 (FSTTCS, 2021)

A Proof Method for Local Sufficient Completeness of Term Rewriting Systems. - Tomoki Shiraishi; Kentaro Kikuchi; Takahito Aoto 001 (ICTAC, 2021)

Commutative Rational Term Rewriting. - Mamoru Ishizuka; Takahito Aoto 001; Munehiro Iwami (LATA, 2021)

A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems. - Ryota Haga; Yuki Kagaya; Takahito Aoto 001 (FroCoS, 2023)

Equational Theories and Validity for Logically Constrained Term Rewriting. - Takahito Aoto 001; Naoki Nishida 001; Jonas Schöpf (FSCD, 2024)

Proving Uniqueness of Normal Forms w.r.t Reduction of Term Rewriting Systems. - Takahito Aoto 001 (LOPSTR, 2024)

Equational Theories and Validity for Logically Constrained Term Rewriting (Full Version). - Takahito Aoto 001; Naoki Nishida 001; Jonas Schöpf (CoRR, 2024)

Characterizing Equivalence of Logically Constrained Terms via Existentially Constrained Terms (Full Version). - Kanta Takahata; Jonas Schöpf; Naoki Nishida 001; Takahito Aoto 001 (CoRR, 2025)

Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations (Full Version). - Kanta Takahata; Jonas Schöpf; Naoki Nishida 001; Takahito Aoto 001 (CoRR, 2025)