@inproceedings(mu-term,
 author       = {Beatriz Alarc{\'o}n and Ra{\'u}l Guti{\'e}rrez and Salvador Lucas and Navarro-Marset, Rafael},
 year         = {2011},
 title        = {Proving Termination Properties with {MU-TERM}},
 booktitle    = {Proc.\ 13thAlgebraic Methodology and Software Technology},
 series       = {Lecture Notes in Computer Science},
 volume       = {6486},
 pages        = {201--208},
 doi          = {10.1007/978-3-642-17796-5\_12},
)
@inproceedings(ACP,
 author       = {Takahito Aoto and Junichi Yoshida and Yoshihito Toyama},
 year         = {2009},
 title        = {Proving Confluence of Term Rewriting Systems Automatically},
 booktitle    = {Proc.\ 20th International Conference on Rewriting Techniques and Applications},
 series       = {Lecture Notes in Computer Science},
 volume       = {5595},
 pages        = {93--102},
 doi          = {10.1007/978-3-642-02348-4\_7},
)
@inproceedings(AMS16,
 author       = {Martin Avanzini and Georg Moser and Michael Schaper},
 year         = {2016},
 title        = {{TcT}: {T}yrolean {C}omplexity {T}ool},
 booktitle    = {Proc.\ 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {9636},
 publisher    = {Springer},
 pages        = {407--423},
 doi          = {10.1007/978-3-662-49674-9\_24},
)
@book(BN98,
 author       = {Franz Baader and Tobias Nipkow},
 year         = {1998},
 title        = {Term Rewriting and All That},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139172752},
)
@inproceedings(DT90,
 author       = {Max Dauchet and Sophie Tison},
 year         = {1990},
 title        = {The Theory of Ground Rewrite Systems is Decidable},
 booktitle    = {Proc.\ 5th IEEE Symposium on Logic in Computer Science},
 pages        = {242--248},
 doi          = {10.1109/LICS.1990.113750},
)
@incollection(DP01,
 author       = {Nachum Dershowitz and David A. Plaisted},
 year         = {2001},
 title        = {Chapter 9 -- Rewriting},
 booktitle    = {Handbook of Automated Reasoning},
 publisher    = {North-Holland},
 pages        = {535--610},
 doi          = {10.1016/B978-044450813-3/50011-4},
)
@inproceedings(Fu19,
 author       = {Carsten Fuhs},
 year         = {2019},
 title        = {Transforming Derivational Complexity of Term Rewriting to Runtime Complexity},
 booktitle    = {Proc.\ 12th International Workshop on Frontiers of Combining Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {11715},
 publisher    = {Springer},
 pages        = {348--364},
 doi          = {10.1007/978-3-030-29007-8\_20},
)
@article(AProVE,
 author       = {J{\"u}rgen Giesl and Cornelius Aschermann and Marc Brockschmidt and Fabian Emmes and Florian Frohn and Carsten Fuhs and Jera Hensel and Carsten Otto and Martin Pl{\"u}cker and Schneider-Kamp, Peter and Thomas Ströder and Stephanie Swiderski and René Thiemann},
 year         = {2017},
 title        = {Analyzing Program Termination and Complexity Automatically with {AProVE}},
 journal      = {Journal of Automated Reasoning},
 volume       = {58},
 number       = {1},
 pages        = {3--31},
 doi          = {10.1007/s10817-016-9388-y},
)
@inproceedings(HNM18,
 author       = {Nao Hirokawa and Julian Nagele and Aart Middeldorp},
 year         = {2018},
 title        = {Cops and {CoCoWeb} -- {I}nfrastructure for Confluence Tools},
 booktitle    = {Proc.\ 9th International Joint Conference on Automated Reasoning},
 series       = {Lecture Notes in Artificial Intelligence},
 volume       = {10900},
 publisher    = {Springer},
 pages        = {346--353},
 doi          = {10.1007/978-3-319-94205-6\_23},
)
@inproceedings(HL89,
 author       = {Dieter Hofbauer and Clemens Lautemann},
 year         = {1989},
 title        = {Termination Proofs and the Length of Derivations},
 booktitle    = {Proc.\ 3rd International Conference on Rewriting Techniques and Applications},
 series       = {Lecture Notes in Computer Science},
 volume       = {355},
 publisher    = {Springer},
 pages        = {167--177},
 doi          = {10.1007/3-540-51081-8\_107},
)
@inproceedings(maxcomp,
 author       = {Dominik Klein and Nao Hirokawa},
 year         = {2011},
 title        = {Maximal Completion},
 booktitle    = {Proc.\ 22nd International Conference on Rewriting Techniques and Applications},
 series       = {Leibniz International Proceedings in Informatics},
 volume       = {10},
 pages        = {71--80},
 doi          = {10.4230/LIPIcs.RTA.2011.71},
)
@incollection(KB70,
 author       = {Donald E. Knuth and Peter B. Bendix},
 year         = {1970},
 title        = {Simple Word Problems in Universal Algebras},
 editor       = {J. Leech},
 booktitle    = {Computational Problems in Abstract Algebra},
 publisher    = {Pergamon Press},
 pages        = {263--297},
 doi          = {10.1016/B978-0-08-012975-4.50028-X},
)
@inproceedings(wanda,
 author       = {Cynthia Kop},
 year         = {2019},
 title        = {A short overview of {Wanda}},
 booktitle    = {Joint Proceedings of the 10th Workshop on Higher-Order Rewriting and the 8th International Workshop on Confluence},
 pages        = {21--25},
 note         = {Available from \url{http://cl-informatik.uibk.ac.at/iwc/hor-iwc2019.pdf}},
)
@inproceedings(KSZM09,
 author       = {Martin Korp and Christian Sternagel and Harald Zankl and Aart Middeldorp},
 year         = {2009},
 title        = {Tyrolean Termination Tool 2},
 booktitle    = {Proc.\ 20th International Conference on Rewriting Techniques and Applications},
 series       = {Lecture Notes in Computer Science},
 volume       = {5595},
 publisher    = {Springer},
 pages        = {295--304},
 doi          = {10.1007/978-3-642-02348-4\_21},
)
@inproceedings(MNS19,
 author       = {Aart Middeldorp and Julian Nagele and Kiraku Shintani},
 year         = {2019},
 title        = {Confluence Competition 2019},
 booktitle    = {Proc.\ 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {11429},
 publisher    = {Springer},
 pages        = {25--40},
 doi          = {10.1007/978-3-030-17502-3\_2},
)
@mastersthesis(M18,
 author       = {Fabian Mitterwallner},
 year         = {2018},
 title        = {Automating Rewrite Strategies},
 type         = {bachelor thesis},
 school       = {University of Innsbruck},
)
@inproceedings(NFM17,
 author       = {Julian Nagele and Bertram Felgenhauer and Aart Middeldorp},
 year         = {2017},
 title        = {{CSI}: New Evidence -- A Progress Report},
 booktitle    = {Proc.\ 26th International Conference on Automated Deduction},
 series       = {Lecture Notes in Artificial Intelligence},
 volume       = {10395},
 publisher    = {Springer},
 pages        = {385--397},
 doi          = {10.1007/978-3-319-63046-5\_24},
)
@article(N42,
 author       = {Max H. A. Newman},
 year         = {1942},
 title        = {On Theories with a Combinatorial Definition of Equivalence},
 journal      = {Annals of Mathematics},
 volume       = {43},
 number       = {2},
 pages        = {223--243},
 doi          = {10.2307/1968867},
)
@incollection(OV03,
 author       = {{Vincent van} Oostrom and {Roel de} Vrijer},
 year         = {2003},
 title        = {Strategies},
 editor       = {Terese},
 booktitle    = {Term Rewriting Systems},
 series       = {Cambridge Tracts in Theoretical Computer Science},
 volume       = {55},
 publisher    = {Cambridge University Press},
 chapter      = {9},
 pages        = {475--547},
)
@article(NTI,
 author       = {{\'E}tienne Payet and Frédéric Mesnard},
 year         = {2006},
 title        = {Nontermination Inference of Logic Programs},
 journal      = {ACM Transactions on Programming Languages and Systems},
 volume       = {28},
 number       = {2},
 pages        = {256--289},
 doi          = {10.1145/1119479.1119481},
)
@article(PS81,
 author       = {Gerald E. Peterson and Mark E. Stickel},
 year         = {1981},
 title        = {Complete Sets of Reductions for Some Equational Theories},
 journal      = {Journal of the ACM},
 volume       = {28},
 number       = {2},
 pages        = {233--264},
 doi          = {10.1145/322248.322251},
)
@inproceedings(vdP01,
 author       = {{Jaco van de} Pol},
 year         = {2001},
 title        = {Just-in-time: On Strategy Annotations},
 booktitle    = {Proc.\ 1st International Workshop on Reduction Strategies in Rewriting and Programming},
 series       = {Electronic Notes in Theoretical Computer Science},
 volume       = {57},
 pages        = {41--63},
 doi          = {10.1016/S1571-0661(04)00267-1},
)
@inproceedings(vdP02,
 author       = {{Jaco van de} Pol},
 year         = {2002},
 title        = {{JITty}: A Rewriter with Strategy Annotations},
 booktitle    = {Proc.\ 13th International Conference on Rewriting Techniques and Applications},
 series       = {Lecture Notes in Computer Science},
 volume       = {2378},
 publisher    = {Springer},
 pages        = {367--370},
 doi          = {10.1007/3-540-45610-4_26},
)
@article(NWT05,
 author       = {Prijsvraag},
 year         = {2015},
 title        = {Het Cola-gen},
 journal      = {Natuur, Wetenschap \& Techniek},
 volume       = {73},
 number       = {1},
 pages        = {65},
)
@inproceedings(RM16,
 author       = {Franziska Rapp and Aart Middeldorp},
 year         = {2016},
 title        = {Automating the First-Order Theory of Left-Linear Right-Ground Term Rewrite Systems},
 booktitle    = {Proc.\ 1st International Conference on Formal Structures for Computation and Deduction},
 series       = {Leibniz International Proceedings in Informatics},
 volume       = {52},
 publisher    = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
 pages        = {36:1--36:12},
 doi          = {10.4230/LIPIcs.FSCD.2016.36},
)
@inproceedings(RM18,
 author       = {Franziska Rapp and Aart Middeldorp},
 year         = {2018},
 title        = {{FORT} 2.0},
 booktitle    = {Proc.\ 9th International Joint Conference on Automated Reasoning},
 series       = {Lecture Notes in Artificial Intelligence},
 volume       = {10900},
 publisher    = {Springer},
 pages        = {81--88},
 doi          = {10.1007/978-3-319-94205-6\_6},
)
@article(R73,
 author       = {Barry K. Rosen},
 year         = {1973},
 title        = {Tree-Manipulating Systems and Church-Rosser Theorems},
 journal      = {Journal of the ACM},
 volume       = {20},
 number       = {1},
 pages        = {160--187},
 doi          = {10.1145/321738.321750},
)
@article(SS18,
 author       = {Jonas Sch{\"{o}}pf and Christian Sternagel},
 year         = {2018},
 title        = {{TTT2} with Termination Templates for Teaching},
 journal      = {The Computing Research Repository},
 volume       = {abs/1806.05040},
 url          = {http://arxiv.org/abs/1806.05040},
)
@inproceedings(CollSaigawa,
 author       = {Kiraku Shintani and Nao Hirokawa},
 year         = {2019},
 title        = {{CoLL-Saigawa} 1.3: A Joint Confluence Tool},
 booktitle    = {Joint Proceedings of the 10th Workshop on Higher-Order Rewriting and the 8th International Workshop on Confluence},
 pages        = {57},
 note         = {Available from \url{http://cl-informatik.uibk.ac.at/iwc/hor-iwc2019.pdf}},
)
@inproceedings(ST14,
 author       = {Christian Sternagel and Ren\'{e} Thiemann},
 year         = {2014},
 title        = {The Certification Problem Format},
 booktitle    = {Proc.\ 11th Workshop on User Interfaces for Theorem Provers (UITP)},
 series       = {Electronic Proceedings in Computer Science},
 volume       = {167},
 pages        = {61--72},
 doi          = {10.4204/EPTCS.167.8},
)
@inproceedings(SZ12,
 author       = {Thomas Sternagel and Harald Zankl},
 year         = {2012},
 title        = {{KBCV} -- {K}nuth--{B}endix Completion Visualizer},
 booktitle    = {Proc.\ 6th International Joint Conference on Automated Reasoning},
 series       = {Lecture Notes in Artificial Intelligence},
 volume       = {7364},
 pages        = {530--536},
 doi          = {10.1007/978-3-642-31365-3_41},
)
@book(TeReSe,
 editor       = {Terese},
 year         = {2003},
 title        = {Term Rewriting Systems},
 series       = {Cambridge Tracts in Theoretical Computer Science},
 volume       = {55},
 publisher    = {Cambridge University Press},
)
@inproceedings(CETA,
 author       = {Ren\'e Thiemann and Christian Sternagel},
 year         = {2009},
 title        = {Certification of Termination Proofs using {CeTA}},
 booktitle    = {Proc.\ 22th International Conference on Theorem Proving in Higher Order Logics},
 series       = {Lecture Notes in Computer Science},
 volume       = {5674},
 publisher    = {Springer},
 pages        = {452--468},
 doi          = {10.1007/978-3-642-03359-9_31},
)
@inproceedings(To98,
 author       = {H{\'e}l{\`e}ne Touzet},
 year         = {1998},
 title        = {Encoding the {H}ydra Battle as a Rewrite System},
 booktitle    = {Proc.\ 23rd Mathematical Foundations of Computer Science},
 series       = {Lecture Notes in Computer Science},
 volume       = {1450},
 publisher    = {Springer},
 pages        = {267--276},
 doi          = {10.1007/BFb0055776},
)
@inproceedings(maedmax,
 author       = {Sarah Winkler and Georg Moser},
 year         = {2018},
 title        = {MaedMax: A Maximal Ordered Completion Tool},
 booktitle    = {Proc.\ 9th International Joint Conference on Automated Reasoning},
 series       = {Lecture Notes in Computer Science},
 volume       = {10900},
 pages        = {472--480},
 doi          = {10.1007/978-3-319-94205-6\_31},
)
@article(WSMK13,
 author       = {Sarah Winkler and Haruhiko Sato and Aart Middeldorp and Masahito Kurihara},
 year         = {2013},
 title        = {Multi-Completion with Termination Tools},
 journal      = {Journal of Automated Reasoning},
 volume       = {50},
 number       = {3},
 pages        = {317--354},
 doi          = {10.1007/s10817-012-9249-2},
)
@inproceedings(NaTT,
 author       = {Akihisa Yamada and Keiichirou Kusakari and Toshiki Sakabe},
 year         = {2014},
 title        = {Nagoya Termination Tool},
 booktitle    = {Proc.\ 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications},
 series       = {Lecture Notes in Computer Science},
 volume       = {8560},
 pages        = {466--475},
 doi          = {10.1007/978-3-319-08918-8_32},
)
@inproceedings(ZFM11,
 author       = {Harald Zankl and Bertram Felgenhauer and Aart Middeldorp},
 year         = {2011},
 title        = {{CSI} -- {A} Confluence Tool},
 booktitle    = {Proc.\ 22nd International Conference on Automated Deduction},
 series       = {Lecture Notes in Artificial Intelligence},
 volume       = {6803},
 publisher    = {Springer},
 pages        = {499--505},
 doi          = {10.1007/978-3-642-22438-6\_38},
)
@article(ZWM15,
 author       = {Harald Zankl and Sarah Winkler and Aart Middeldorp},
 year         = {2015},
 title        = {Beyond Polynomials and {P}eano Arithmetic -- Automation of Elementary and Ordinal Interpretations},
 journal      = {Journal of Symbolic Computation},
 volume       = {69},
 pages        = {129--158},
 doi          = {10.1016/j.jsc.2014.09.033},
)