Publications of ToyamaAoto Laboratory
 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.237248, ACM Press.
 Tatsunari Nakazima, Takahito Aoto and Yoshihito Toyama,
Decidability of inductive theorems based on rewriting induction (in Japanese),
Computer Software, Vol.31, No.3, pp.294306, 2014.
 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 (RTATLCA 2014), Vienna, Austria, LNCS 8560, pp.4660, 2014.
 Kentaro Kikuchi,
Uniform Proofs of Normalisation and Approximation for Intersection
Types,
In Proceedings of the 7th Workshop on Intersection Types and
Related Systems (ITRS 2014), Vienna, Austria, 2014.
 Kentaro Kikuchi and Takafumi Sakurai,
A Translation of Intersection and Union Types for the
λμCalculus,
In Proceedings of the 5th International Workshop on Classical Logic
and Computation (CL&C 2014), Vienna, Austria, 2014.
 Shota Takahashi, Takahito Aoto and Yoshihito Toyama,
Innermost reachability of bottomup innermost term rewriting systems (in Japanese),
Computer Software, Vol.31, No.1, pp.7589, 2014.
 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, LNAI 8152, pp.311326, 2013.
 Kentaro Kikuchi,
Proving strong normalisation via nondeterministic translations into Klop's extended λcalculus,
In Proceedings of the 22nd Annual Conference of the European Association for Computer Science Logic (CSL 2013), LIPIcs 23, pp.395414, 2013.

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.148162, 2013.
 Takahito Aoto,
Disproving confluence of term rewriting systems by interpretation and ordering (extended abstract),
In Proceedings of the 2nd International Workshop on Confluence (IWC 2013),
Eindhoven, The Netherlands, pp.59, 2013

Takahito Aoto and Munehiro Iwami,
Termination of rulebased calculi for uniform semiunification,
In Proceedings of the 7th International Conference on Language and Automata
Theory and Applications (LATA 2013), Bilbao, Spain, LNCS 7810, pp.5667, 2013.

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.187202, 2013.

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, LNCS 7562, pp.172186, 2012.

Yuki Chiba and Takahito Aoto,
Transformations by templates for simplytyped term rewriting,
In Proceedings of the 6th International Workshop on HigherOrder
Rewriting (HOR 2012),
Nagoya, Japan, June 2012, pp.38.

Takahito Aoto and Yoshihito Toyama,
A reductionpreserving completion for proving confluence of nonterminating
term rewriting systems,
Logical Methods in Computer Science, Vol.8, No.1:31, pp.129, 2012.

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.211239, 2012.

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.176190, 2012.

Takahito Aoto, Toshiyuki Yamada and Yuki Chiba,
Natural inductive theorems for higherorder rewriting,
In Proceedings of the 22nd International Conference on Rewriting
Techniques and Applications (RTA 2011), Novi Sad, Serbia,
Leibniz International Proceedings in Informatics,
Vol.10, pp.107121, 2011.

Takahito Aoto and Yoshihito Toyama,
Reductionpreserving completion for proving confluence of
nonterminating term rewriting systems,
In Proceedings of the 22nd International Conference on Rewriting
Techniques and Applications (RTA 2011), Novi Sad, Serbia,
Leibniz International Proceedings in Informatics,
Vol.10, pp.91106, 2011.

Takahito Aoto,
Automated confluence proof by decreasing diagrams based on rulelabelling,
In Proceedings of the 21st International Conference on
Rewriting Techniques and Applications (RTA 2010),
Edingburgh, UK,
Leibniz International Proceedings in Informatics, Vol.6, pp.716, 2010.

Yuki Chiba, Takahito Aoto and Yoshihito Toyama,
Program transformation templates for tupling based on term rewriting,
IEICE Transactions on Information and Systems,
Vol.E93D, No.5, pp.963973, 2010.

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, LNAI 5749,
pp.117132, 2009.

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, LNCS 5595,
pp.93102, 2009.

Junichi Yoshida, Takahito Aoto, Yoshihito Toyama,
Automating Confluence Check of Term Rewriting Systems (in Japanese),
Computer Software, Vol.26, No.2, pp.7692, 2009.
crexamples080920.tgz

Satoshi Shimazu, Takahito Aoto, Yoshihito Toyama,
Automated Lemma Generation for Rewriting Induction with Disproof (in Japanese),
Computer Software, Vol.26, No.2, pp.4155, 2009.

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,
LIPIcs, Vol.2,
pp.1324, 2008.

JeanPierre Jouannaud and Yoshihito Toyama,
Modular ChurchRosser Modulo: The Complete Picture,
International Journal of Software and Informatics,
Vol.2, No.1, pp.6175, 2008.

Yoshihito Toyama,
Termination proof of Sexpression rewriting systems
with recursive path relations,
In Proceedings of the 19th International Conference on Rewriting
Techniques and Applications (RTA 2008), Hagenberg, Austria,
LNCS 5117, pp.381391, 2008.

Jeroen Ketema,
On normalisation of infinitary combinatory reduction systems,
In Proceedings of the 19th International Conference on Rewriting
Techniques and Applications (RTA 2008), Hagenberg, Austria,
LNCS 5117, pp.172186, 2008.

Takahito Aoto,
Designing a rewriting induction prover with an increased
capability of nonorientable theorems,
In Proceedings of AustrianJapanese Workshop on
Symbolic Computation in Software Science (SCSS 2008),
Hagenberg, Austria, pp.115, 2008

Kentaro Kikuchi,
CallbyName Reduction and CutElimination in Classical Logic,
Annals of Pure and Applied Logic, Vol.153, No.13, pp.3865, 2008.

Kentaro Kikuchi and Stéphane Lengrand,
Strong Normalisation of CutElimination that Simulates βReduction,
In Proceedings of the 11th International Conference on Foundations of
Software Science and Computation Structures (FoSSaCS 2008),
LNCS 4962, pp.380394, 2008.

Yuki Chiba,
A Term Rewriting Approach to Program Transformation by Templates,
Ph.D. Thesis, Tohoku University, 2008.

Takahito Aoto,
Soundness of rewriting induction based on an abstract principle,
IPSJ Transactions on Programming, Vol.49, No.SIG 1 (PRO 35), pp.2838, 2008.

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.1427, 2008.

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.3134, 2007.

Ryo Ishigaki and Kentaro Kikuchi,
TreeSequent Methods for Subintuitionistic Predicate Logics,
In Proceedings of the 16th International Conference on Automated Reasoning
with Analytic Tableaux and Related Methods (TABLEAUX 2007), LNAI 4548, pp.149164, 2007.

Kentaro Kikuchi,
Simple Proofs of Characterizing Strong Normalization
for Explicit Substitution Calculi,
In Proceedings of the 18th International Conference on Rewriting
Techniques and Applications (RTA 2007), LNCS 4533, pp.257272, 2007.

Joerg Endrullis and Jeroen Ketema,
Root Stabilisation Using Dependency Pairs,
In Proceedings of the 9th International Workshop on Termination (WST 2007),
pp.1721, 2007.

Takahito Aoto and Toshiyuki Yamada,
Argument filterings and usable rules for
simply typed dependency pairs (extended abstract),
In Proceedings of the 4th International Workshop on
HigherOrder Rewriting (HOR 2007), Paris, France, pp.2127, 2007.

Kentaro Kikuchi,
Confluence of CutElimination Procedures for the
Intuitionistic Sequent Calculus,
In Proceedings of the 3rd Conference on Computability in
Europe (CiE 2007), LNCS 4497, pp.398407, 2007.

Ryo Ishigaki and Kentaro Kikuchi,
A TreeSequent Calculus for a Natural Predicate Extension
of Visser's Propositional Logic,
Logic Journal of the Interest Group in Pure and Applied Logics, Vol.15, No.2, pp.149164, 2007.

Keiichirou Kusakari, and Yuki Chiba,
A HigherOrder KnuthBendix Procedure and its Applications,
IEICE Transactions on Information and Systems,
Vol.E90D, No.4, pp.707715, Apr 2007.

Kentaro Kikuchi,
On a LocalStep CutElimination Procedure for the
Intuitionistic Sequent Calculus,
In Proceedings of the 13th International
Conference on Logic for Programming, Artificial Intelligence and Reasoning
(LPAR 2006), LNAI 4246, pp.120134, 2006.

KUSAKARI Keiichirou, NAKAMURA Masaki, TOYAMA Yoshihito,
Elimination Transformations for AssociativeCommutative Rewriting Systems,
Journal of Automated Reasoning, Vol.37, No.3, pp.205229, Oct 2006.

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.5265,
2006.

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, Lecture Notes in Computer Science,
Vol.4098, SpringerVerlag, pp.267276, 2006.

Takahito Aoto,
Dealing with Nonorientable Equations in Rewriting Induction,
In Proceedings of the 17th International Conference on
Rewriting Techniques and Applications (RTA 2006),
Seattle, WA, USA, Lecture Notes in Computer Science,
Vol.4098, SpringerVerlag, pp.242256, 2006.

Kentaro Kikuchi,
CallbyName Reduction and CutElimination in Classical Logic,
In Proceedings of the 1st International Workshop on
Classical Logic and Computation (CL&C 2006), 2006.

Yoshihito Toyama,
Reduction strategies for leftlinear term rewriting systems,
In Processes, Terms and Cycles: Steps on the Road to Infinity,
Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th
Birthday,
Lecture Notes in Computer Science, Vol.3838, pp.198223, 2005.

Yuki Chiba, Takahito Aoto and Yoshihito Toyama,
Introducing Sequence Variables in Program Transformation based on
Templates,
In Proceedings of the Forum on Information Technology 2005 (FIT2005),
Information Technology Letters, Vol.4, pp.58, 2005 (in Japanese).

Yuki Chiba, Takahito Aoto and Yoshihito Toyama,
Program Transformation by Templates based on Term Rewriting,
In Proceedings of the 7th ACMSIGPLAN International Symposium
on Principles and Practice of Declarative Programming (PPDP 2005), ACP Press, pp.5969, 2005.

Yoshihito Toyama,
Confluent Term Rewriting Systems, Invited Talk,
In Proceedings of the 16th International Conference on
Rewriting Techniques and Applications (RTA 2005), Nara, Japan,
Lecture Notes in Computer Science, Vol.3467, SpringerVerlag, p.1,
2005.
[Slide]

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,
Lecture Notes in Computer Science, Vol.3467, SpringerVerlag, pp.120134, 2005.

Y.Toyama,
Termination of Sexpression rewriting systems:
Lexicographic path ordering for higherorder terms,
In Proceedings of the 15th International Conference
on Rewriting Techniques and Applications (RTA 2004),
Aachen, Germany,
Lecture Notes in Computer Science, Vol.3091,
SpringerVerlag, pp.4054, 2004.

T.Aoto, T.Yamada and Y.Toyama,
Inductive theorems for higherorder rewriting,
In Proceedings of the 15th International Conference
on Rewriting Techniques and Applications (RTA 2004),
Aachen, Germany,
Lecture Notes in Computer Science, Vol.3091,
SpringerVerlag, pp.269284, 2004.

T.Aoto and T.Yamada,
Termination of simplytyped applicative term rewriting systems,
In Proceedings of the 2nd International Workshop on
HigherOrder Rewriting (HOR 2004), Aachen, Germany,
Technical Report 200403,
Department of Computer Science, RWTH Aachen, pp.6165, 2004.

Takahito Aoto, Toshiyuki Yamada and Yoshihito Toyama,
Proving inductive theorems of higherorder functional programs,
In Proceedings of the Forum on Information Technology 2003 (FIT2003),
Information Technology Letters, Vol.2, pp.2122, 2003
(in Japanese).

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,
Valencia, Spain,
Lecture Notes in Computer Science, Vol.2706, SpringerVerlag
pp.380394, 2003.

T.Aoto and T.Yamada,
Proving Termination of Simply Typed Term Rewriting Systems Automatically,
IPSJ Trans. Programming, Vol. 44, No.SIG 4 (PRO17), pp.6777, 2003
(in Japanese).

T.Nagaya and Y.Toyama,
Decidability for leftlinear growing term rewriting systems,
Information and Computation Vol.178, (2002) 499514.

M.Sakai and K.Kusakari,
On Proving Termination of HigherOrder Rewrite Systems
by Dependency Pair technique,
The First International Workshop on HigherOrder Rewriting (HOR'02),
Copenhagen, Denmark, July 21, p.25(2002).

M.Sakai and K.Kusakari,
On New Dependency Pair Method for Proving Termination
of HigherOrder Rewrite Systems,
The International Workshop on Rewriting in Proof and Computation (RPC'01),
Sendai, Japan, October 2527, pp.176187(2001).

Y.Toyama,
Equational Proofs by Completion,
Journal of Japanese Society for Artificial Intelligence,
Vol.16, No.5, pp.668674, 2001 (Survey Paper; in Japanese).

K.Kusakari,
On Proving Termination of Term Rewriting Systems
with HigherOrder Variables,
IPSJ Transactions on Programming,
Vol.42, No.SIG 7 (PRO 11), pp.3545, 2001.

K.Kusakari, Y.Toyama,
On Proving ACTermination by ACDependency Pairs,
IEICE Transactions on Information and Systems,
Vol.E84D, No.5, pp.604612, 2001.
[draft]

Y.Toyama and M.Oyamaguchi,
ChurchRosser Property and Unique Normal Form Property
of NonDuplicating Term Rewriting Systems,
IEICE Transactions on Information and Systems,
Vol.E84D, No.4, pp.439447, 2001.

Taro Suzuki and Aart Middeldorp,
A Complete Selection Function for Lazy Conditional Narrowing,
FLOPS'01, Proceedings of the 5th International Symposium
on Functional and Logic Programming,
Lecture Notes in Computer Science 2024, pp.201215, 2001.

Y.Toyama,
New Challenges for Computational Models,
Proc. of Int. Conf. IFIP Theoretical Computer Science,
Lecture Notes in Computer Science 1872, pp.612613, 2000 (Panel Discussion).

H.Koike, Y.Toyama,
Comparison between Inductionless Induction and Rewriting Induction,
JSSST Computer Software Vol.17, No.6, pp.112, 2000 (in Japanese).

K.Kusakari, Y.Toyama,
On Proving ACTermination by Argument Filtering Method,
IPSJ Transactions on Programming,
Vol.41, No.SIG 4 (PRO 7), pp.6578, 2000.
Publications of Toyama Laboratory
in JAIST (1997.42000.3)

K.Kusakari,
Termination, ACTermination and Dependency Pairs
of Term Rewriting Systems,
Ph.D. Thesis, JAIST, 2000.

Mircea Marin, Tetsuo Ida, and Taro Suzuki,
On Reducing the Search Space of HigherOrder Lazy Narrowing,
FLOPS'99, Proceedings of the 4th International Symposium
on Functional and Logic Programming,
Lecture Notes in Computer Science 1722, pp.319334, 1999.

M.Nakamura, K.Kusakari, Y.Toyama,
On Proving Termination by General Dummy Elimination,
IEICE Transactions on Information and Systems,
Vol. J82DI, No.10, pp.12251231, 1999 (in Japanese).

K.Kusakari, M.Nakamura, Y.Toyama,
Argument Filtering Transformation,
In Proceedings of International Conference on
Principles and Practice of Declarative Programming,
LNCS 1702 (PPDP'99), pp.4761, 1999.

Munehiro Iwami,
Termination of HigherOrder Rewrite Systems,
Ph.D. Thesis, JAIST, 1999.

Takashi Nagaya,
Reduction Strategies for Term Rewriting Systems,
Ph.D. Thesis, JAIST, 1999.

Mohamed Hamada, Aart Middeldorp and Taro Suzuki,
Completeness Results for a Lazy Conditional Narrowing Calculus,
DMTCS'99, Proceedings of
Discrete Mathematics and Theoretical Computer Science, 1999.

M. Iwami, Y. Toyama,
Simplification ordering for higherorder rewrite systems,
IPSJ Trans. on Programming, Vol.40, No.SIG 4 (PRO 3), pp.110, 1999.

M. Iwami, M. Sakai, Y. Toyama,
An improved recursive decomposition ordering for
higherorder rewrite systems,
Trans. of IEICE, Vol. E81D, No. 9, pp. 988996, 1998.

Masahiko Sakai, Yoshihito Toyama,
Semantics and Strong Sequentiality
of Priority Term Rewriting Systems,
Theoretical Computer Science, Vol.208, pp.87110(1998).

T. Aoto, Y. Toyama,
Termination transformation by tree lifiting ordering,
in Proc. of the 9th International Conference
on Rewrite Techniques and Applications (RTA'98),
LNCS 1379, pp. 256270, 1998.

T. Aoto, Y. Toyama,
Persistency of confluence,
Journal of Universal Computer Science,
Vol. 3, No. 11, pp. 11341147, 1997.

T. Aoto, Y. Toyama,
On composable properties of term rewriting systems,
in Proc. of the 6th International Joint Conference,
ALP'97  HOA'97, LNCS Vol. 1298, pp. 114128, 1997.
Publications of Toyama and
Sakai Laboratory
in JAIST (1993.41997.3)

M. Sakai, Y. Toyama,
Semantics and strong sequentiality of priority term rewriting systems,
in Proc. of the 7th International Conference
on Rewrite Techniques and Applications (RTA'96),
LNCS Vol. 1103, pp. 377391, 1996.

Y. Takahashi, M. Sakai, Y. Toyama,
On the confluence property of conditional term rewriting systems,
Trans. of IEICE, Vol. J79DI, No. 11, pp. 16, 1996 (in Japanese).

Y. Ohta, M. Oyamaguchi, Y. Toyama,
On the confluence property of siplerightlinear TRS's
Trans. of IEICE, Vol. J78DI, No. 3, pp. 263268, 1995 (in Japanese).

Y. Toyama, J. W. Klop, H. P. Barendregt,
Termination for direct sums of
leftlinear complete term rewriting systems,
Journal of the Association for Computer Machinery,
Vol. 42, No. 6, pp. 12751304, 1995.

S. Yamamoto, R. Ishikawa, M. Sakai, K. Agusa,
An implimentation of TRS on shared memory multiprocessorts,
Trans. of IEICE, Vol. J78DI, No. 6, pp. 559562, 1995 (in Japanese).

Y. Hamaguchi, M. Sakai, S. Yamamoto, K. Agusa,
Error Description on Algebraic Specification and its Automatic Addition,
Trans. of IEICE, Vol. J78DI, No. 3, pp. 323330, 1995 (in Japanese).

M. Kawakita, M. Sakai, S. Yamamoto, K. Agusa,
A model for reuse based on formal specifications,
Trans. of IPSJ, Vol. 36, No. 5, 1995 (in Japanese).

Y. Ohta, M. Oyamaguchi, Y. Toyama,
On the confluence property of siplerightlinear TRS's
Trans. of IEICE, Vol. J78DI, No. 3, pp. 263268, 1995 (in Japanese).

J. W. Klop, A. Middeldorp, Y. Toyama, R. de Vrijer,
Modularity of confluence: A simplified proof,
Information Processing Letters,
Vol. 49, pp. 101109, 1994.

Y. Toyama, M. Oyamaguchi
ChurchRosser property and unique normal formal property
of nonduplicating term rewriting systems,
in Proc. of the 4th International Conference
on Conditional and Typed Rewrite Systems (CTRS'94),
LNCS Vol. 968, pp. 316331, 1994.

Y. Toyama, S. Smetsers, M. Eeklen, R. Plasmeijer,
The functional strategy and transitive term rewriting systems,
in Term Graph Rewriting (M. R. Sleep, etc., eds., Wiley, 1993),
pp. 6175, 1993.
[ToyamaAoto Lab.]
[
RIEC]
[Tohoku University]
Please send any requests and comments to
webmaster