Other publications
Selected Publications
 Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama,
Parallel Closure Theorem for LeftLinear Nominal Rewriting Systems,
In Proceedings of the
11th International Symposium on Frontiers of Combining Systems
(FroCoS 2017),
Blasilia, Blazil,
Lecture Notes in Computer Science,
to appear.
 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,
Leibniz International Proceedings in Informatics,
to appear.
 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.93107, 2016.
 Vincent van Oostrom and Yoshihito Toyama,
Normalisation by random descent,
In Proceedings of the 1st International Conference on Formal
Structures for Computation and Deduction (FSCD 2016),
Porto, Portugal,
Leibniz International Proceedings in Informatics,
Vol.52, pp.32:132:18, 2016.
 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,
Leibniz International Proceedings in Informatics,
Vol.52, pp.33:133:12, 2016.
 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,
EPiC Series in Computing,
Vol.39, pp.156168, 2016.
 Koichi Sato, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama,
Correctness of contextmoving transformations for term rewriting
systems,
In Proceedings of 25th International Symposium on LogicBased Program
Synthesis and Transformation (LOPSTR 2015), Siena, Italy,
Lecture Notes in Computer Science,
Vol.9527, pp.331345, 2015.
 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,
Leibniz International Proceedings in Informatics,
Vol.36, pp.301317, 2015.

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.179193, 2015.

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.

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.

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.

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 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.

Kouki Isobe, Takahito Aoto, Yoshihito Toyama,
A PathOrder of Term Rewriting Systems for PolynomialSize Normal
Forms (in Japanese),
Computer Software, Vol.29, No.1, pp.176190, 2012.

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.

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, Junichi Yoshida, Yoshihito Toyama,
Proving Confluence of Term Rewriting Systems Automatically,
In Proceedings of the 20th International Conference on Rewriting
Techniques and Applications (RTA 2009),
Lecture Notes in Computer Science Vol.5595, pp.93102, 2009.

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

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

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),
Lecture Notes in Computer Science, Vol.5117, pp.381391, 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),
Forum on Information Technology 2007 (FIT 2007),
Information Technology Letters, Vol.6, pp.3134, 2007.

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.

Keiichirou Kusakari, Masaki Nakamura and Yoshihito Toyama,
Elimination Transformations for AssociativeCommutative
Rewriting Systems,
Journal of Automated Reasoning, Vol.37, No.3, pp.205229, 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 Japanese),
Forum on Information Technology 2005 (FIT 2005),
Information Technology Letters, Vol.4, pp.58, 2005.

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 2005), 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),
Lecture Notes in Computer Science, Vol.3467, p.1,
2005.
[Abstract]
[Slide]

Yoshihito 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),
Lecture Notes in Computer Science, Vol.3091, pp.4054, 2004.

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

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

Takashi Nagaya and Yoshihito Toyama,
Decidability for leftlinear growing term rewriting systems,
Information and Computation Vol.178, pp.499514, 2002.

Yoshihito Toyama,
Equational Proofs by Completion: A tutorial (in Japanese),
Journal of Japanese Society for Artificial Intelligence,
Vol.16, No.5, pp.668674, 2001.

Keiichirou Kusakari and Yoshihito Toyama,
On Proving ACTermination by ACDependency Pairs,
IEICE Transactions on Information and Systems,
Vol.E84D, No.5, pp.604612, 2001.

Yoshihito Toyama and Michio 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.

Yoshihito Toyama,
New Challenges for Computational Models (Position Paper),
In Proceedings of IFIP International Conference on
Theoretical Computer Science,
Lecture Notes in Computer Science, Vol.1872, pp.612613, 2000.

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

Keiichirou Kusakari and Yoshihito Toyama,
On Proving ACTermination by Argument Filtering Method,
IPSJ Transactions on Programming,
Vol.41, No.SIG 4 (PRO 7), pp.6578, 2000.

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

Keiichirou Kusakari, Masaki Nakamura and Yoshihito Toyama,
Argument Filtering Transformation,
In Proceedings of International Conference on
Principles and Practice of Declarative Programming (PPDP 99),
Lecture Notes in Computer Science, Vol.1702, pp.4761, 1999.

Munehiro Iwami and Yoshihito Toyama,
Simplification ordering for higherorder rewrite systems,
IPSJ Transactions on Programming,
Vol.40, No.SIG 4 (PRO 3), pp.110, 1999.

Munehiro Iwami, Masahiko Sakai and Yoshihito Toyama,
An improved recursive decomposition ordering for
higherorder rewrite systems,
IEICE Transactions on Information and Systems,
Vol.E81D, No.9, pp.988996, 1998.

Masahiko Sakai and Yoshihito Toyama,
Semantics and strong sequentiality
of priority term rewriting systems,
Theoretical Computer Science, Vol.208, pp.87110, 1998.

Takashi Nagaya, Masahiko Sakai and Yoshihito Toyama,
Index reduction of overlapping strongly sequential systems,
IEICE Transactions on Information and Systems,
Vol.E81D, No.5, pp.419426, 1998.

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),
Lecture Notes in Computer Science, Vol.1379, pp.256270, 1998.

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),
Lecture Notes in Computer Science, Vol.1298, pp.114128, 1997.

Takahito Aoto and Yoshihito Toyama,
Persistency of confluence,
Journal of Universal Computer Science,
Vol.3, No.11, pp.11341147, 1997.

Yositaka Takahashi, Masahiko Sakai and Yoshihito Toyama,
On the confluence property of
conditional term rewriting systems (in Japanese),
IEICE Transactions, Vol.J79DI, No.11, pp.897902, 1996.

Masahiko Sakai and Yoshihito Toyama,
Semantics and strong sequentiality of priority term rewriting systems,
In Proceedings of the 7th International Conference on
Rewriting Techniques and Applications (RTA 96),
Lecture Notes in Computer Science, Vol.1103, pp.377391, 1996.

Yoshikatsu Ohta, Michio Oyamaguchi and Yoshihito Toyama,
On the confluence property of simplerightlinear
term rewriting systems (in Japanese),
IEICE Transactions, Vol.J78DI, No.3, pp.263268, 1995.

Yoshihito Toyama, Jan Willem Klop and Henk Pieter 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.

Jan Willem Klop, Aart Middeldorp, Yoshihito Toyama
and Roel de Vrijer,
Modularity of confluence: A simplified proof,
Information Processing Letters, Vol.49, pp.101109, 1994.

Yoshihito Toyama and Michio Oyamaguchi,
ChurchRosser property and unique normal formal property
of nonduplicating term rewriting systems,
In Proceedings of the 4th International Conference on
Conditional and Typed Rewrite Systems (CTRS 94),
Lecture Notes in Computer Science, Vol.968, pp.316331, 1994.

Aart Middeldorp and Yoshihito Toyama,
Completeness of combination of constructor
systems,
Journal of Symbolic Computation, Vol.15, pp.331348,1993.

Yoshihito Toyama, Sjaak Smetsers, Marko van Eeklen, Rinus Plasmeijer,
The functional strategy and transitive term rewriting systems,
in: M.R. Sleep, etc., eds., Term Graph Rewriting, pp.6175, (Wiley, 1993).

Yoshihito Toyama,
Strong sequentiality of leftlinear overlapping
term rewriting systems,
In Proceedings of the 7th IEEE Symposium on Logic
in Computer Science (LICS 92), pp.274284, 1992.

Yoshihito Toyama,
How to prove equivalence of term rewriting systems without
induction,
Theoretical Computer Science, Vol.90, pp.369390, 1991.

Aart Middeldorp and Yoshihito Toyama,
Completeness of combinations of constructor
systems,
In Proceedings of the 4th International Conference on
Rewriting Techniques and Applications (RTA 91),
Lecture Notes in Computer Science, Vol.488, pp.188198, 1991.

Yoshihito Toyama,
Term rewriting systems and the ChurchRosser property,
Doctoral Thesis, Tohoku University, 1990.

Yoshihito Toyama,
Membership conditional term rewriting systems,
IEICE Transactions, Vol.E72, No.11, pp.12241229, 1989.

Yoshihito Toyama,
Fast KnuthBendix completion with a term rewriting system
compiler,
Information Processing Letters, Vol.32, pp.325328, 1989.

Yoshihito Toyama, Jan Willem Klop and Henk Pieter Barendregt,
Termination for the direct sum of
leftlinear term rewriting systems: Preliminary draft,
In Proceedings of the 3rd International Conference on
Rewriting Techniques and Applications (RTA 89),
Lecture Notes in Computer Science, Vol.355, pp.477491, 1989.

Yoshihito Toyama,
Confluent term rewriting systems with membership conditions,
In Proceedings of the 1st International Workshop on
Conditional Term Rewriting Systems (CTRS 88),
Lecture Notes in Computer Science, Vol.308, pp.228241, 1988.

Yoshihito Toyama,
Commutativity of term rewriting systems,
in: K. Fuchi and L. Kott, eds.,
Programming of Future Generation Computer II,
pp.393407, (NorthHolland, 1988).

Yoshihito Toyama,
Counterexamples to termination for the direct sum of term
rewriting systems,
Information Processing Letters, Vol.25, pp.141143, 1987.

Yoshihito Toyama,
On the ChurchRosser property for
the direct sum of term rewriting systems,
Journal of the Association for Computer Machinery,
Vol.34, No.1, pp.128143, 1987.

Tetsuo Ida, Akira Aiba and Yoshihito Toyama,
T: A simple reduction language based on
combinatory term rewriting,
in: K. Fuchi and M. Nivat, eds.,
Programming of Future Generation Computer I,
pp.217236, (NorthHolland, 1986).

Yoshihito Toyama,
How to prove equivalence of term rewriting systems without induction,
In Proceedings of the 8th International Conference
on Automated Deduction (CADE 86),
Lecture Notes in Computer Science, Vol.230, pp.118127, 1986.

Toshiharu Sugawara and Yoshihito Toyama,
Theory of inductive inference: A tutorial (in Japanese),
Journal of the Society of Instrument and Control Engineers,
Vol.25, No.9, pp.781786, 1986.

Yoshihito Toyama,
On equivalence transformations for term rewriting systems,
In Proceedings of RIMS Symposia on Software Science and Engineering II,
Lecture Notes in Computer Science, Vol.220, pp.4461, 1985.

Yoshihito Toyama,
A comment on call by need (in Japanese),
Journal of Information Processing Society of Japan,
Vol.25, No.3, pp.249251, 1984.

Yoshihito Toyama,
On commutativity of term rewriting systems (in Japanese),
IEICE Transactions, Vol.J66D, No.12, pp.13701375, 1983.

Kokichi Futatsugi and Yoshihito Toyama,
Term rewriting systems and their applications:
A survey (in Japanese),
Journal of Information Processing Society of Japan,
Vol.24, No.2, pp.133146, 1983.

Yoshihito Toyama and Masayuki Kimura,
On Learning automata in nonstationary random
environments,
In Proceedings of IEEE Symposium on Cybernetics and Society,
pp.14821486, 1978.

Yoshihito Toyama and Masayuki Kimura,
On Learning automata in nonstationary random environments (in Japanese),
IEICE Transactions, Vol.J60D, No.12, pp.10851092, 1977.
Other publications
Toyama's page
ToyamaAoto laboratory