`Travelled to:`

1 × Austria

1 × Brazil

1 × Italy

1 × Poland

1 × Portugal

1 × Serbia

1 × USA

2 × Spain

3 × Germany

3 × Japan

3 × United Kingdom

`Collaborated with:`

Y.Toyama T.Yamada ∅ Y.Chiba K.Kikuchi S.Stratulat M.Iwami J.Ketema K.Uchida J.Yoshida T.Suzuki N.Hirokawa J.Nagele N.Nishida H.Zankl T.Taketomi T.Sato Y.Mukaigawa N.Yokoya

`Talks about:`

rewrit (14) term (10) confluenc (8) system (7) induct (5) termin (4) prove (4) base (4) transform (3) theorem (3)

## Person: Takahito Aoto

### DBLP: Aoto_0001:Takahito

### Contributed to:

### Wrote 21 papers:

- CADE-2015-AotoHN0Z #confluence #contest
- Confluence Competition 2015 (TA, NH, JN, NN, HZ), pp. 101–104.
- RTA-2015-SuzukiKAT #confluence #orthogonal #revisited #term rewriting
- Confluence of Orthogonal Nominal Rewriting Systems Revisited (TS, KK, TA, YT), pp. 301–317.
- PPDP-2014-AotoS #induction #proving #theorem
- Decision Procedures for Proving Inductive Theorems without Induction (TA, SS), pp. 237–248.
- RTA-TLCA-2014-AotoTU #confluence #diagrams #proving #term rewriting
- Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams (TA, YT, KU), pp. 46–60.
- LATA-2013-AotoI #calculus #rule-based #termination
- Termination of Rule-Based Calculi for Uniform Semi-Unification (TA, MI), pp. 56–67.
- ICGT-2012-AotoK #confluence #decidability #term rewriting
- Rational Term Rewriting Revisited: Decidability and Confluence (TA, JK), pp. 172–186.
- ICPR-2012-AotoTSMY #estimation #using
- Position estimation of near point light sources using a clear hollow sphere (TA, TT, TS, YM, NY), pp. 3721–3724.
- RTA-2011-AotoT #confluence #proving #term rewriting
- A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems (TA, YT), pp. 91–106.
- RTA-2011-AotoYC #higher-order #induction #theorem
- Natural Inductive Theorems for Higher-Order Rewriting (TA, TY, YC), pp. 107–121.
- RTA-2010-Aoto #automation #confluence #diagrams #proving
- Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling (TA), pp. 7–16.
- RTA-2009-AotoYT #automation #confluence #proving #term rewriting
- Proving Confluence of Term Rewriting Systems Automatically (TA, JY, YT), pp. 93–102.
- RTA-2006-Aoto #equation #induction
- Dealing with Non-orientable Equations in Rewriting Induction (TA), pp. 242–256.
- RTA-2006-ChibaA #named #program transformation #term rewriting
- RAPT: A Program Transformation System Based on Term Rewriting (YC, TA), pp. 267–276.
- PPDP-2005-ChibaAT #program transformation #term rewriting
- Program transformation by templates based on term rewriting (YC, TA, YT), pp. 59–69.
- RTA-2005-AotoY #dependence #term rewriting
- Dependency Pairs for Simply Typed Term Rewriting (TA, TY), pp. 120–134.
- RTA-2004-AotoYT #higher-order #induction #theorem
- Inductive Theorems for Higher-Order Rewriting (TA, TY, YT), pp. 269–284.
- RTA-2003-AotoY #term rewriting #termination
- Termination of Simply Typed Term Rewriting by Translation and Labelling (TA, TY), pp. 380–394.
- ALP-PLILP-1998-Aoto #persistent #problem #term rewriting
- Solution to the Problem of Zantema on a Persistent Property of Term Rewriting Systems (TA), pp. 250–265.
- RTA-1998-AotoT #termination
- Termination Transformation by Tree Lifting Ordering (TA, YT), pp. 256–270.
- ALP-1997-AotoT #composition #on the #term rewriting
- On Composable Properties of Term Rewriting Systems (TA, YT), pp. 114–128.
- IJCAR-2016-AotoK #confluence
- Nominal Confluence Tool (TA, KK), pp. 173–182.