@book(BN98,
 author       = {Franz Baader and Tobias Nipkow},
 year         = {1998},
 title        = {Term Rewriting and All That},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139172752},
)
@misc(TATA,
 author       = {Hubert Comon and Max Dauchet and R\'emi Gilleron and Florent Jacquemard and Denis Lugiez and Christof L\"oding and Sophie Tison and Marc Tommasi},
 year         = {2007},
 title        = {{Tree Automata Techniques and Applications}},
 howpublished = {Available on: \url{http://www.grappa.univ-lille3.fr/tata}},
 note         = {Release October, 12th 2007},
)
@inproceedings(DOS88,
 author       = {Nachum Dershowitz and Mitsuhiro Okada and G. Sivakumar},
 year         = {1988},
 title        = {Canonical Conditional Rewrite Systems},
 booktitle    = {Proceedings of the 9th International Conference on Automated Deduction},
 series       = {Lecture Notes in Computer Science},
 volume       = {310},
 publisher    = {Springer},
 pages        = {538--549},
 doi          = {10.1007/BFb0012855},
)
@inproceedings(DLMMU04,
 author       = {Francisco Dur{\'a}n and Salvador Lucas and Jos{\'e} Meseguer and Claude March{\'e} and Xavier Urbain},
 year         = {2004},
 title        = {Proving termination of membership equational programs},
 booktitle    = {Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation},
 publisher    = {ACM},
 pages        = {147--158},
 doi          = {10.1145/1014007.1014022},
)
@article(FG03,
 author       = {Guillaume Feuillade and Thomas Genet},
 year         = {2003},
 title        = {Reachability in Conditional Term Rewriting Systems},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {86},
 number       = {1},
 pages        = {133--146},
 doi          = {10.1016/S1571-0661(04)80658-3},
)
@article(GR10,
 author       = {Thomas Genet and Vlad Rusu},
 year         = {2010},
 title        = {Equational approximations for tree automata completion},
 journal      = {Journal of Symbolic Computation},
 volume       = {45},
 number       = {5},
 pages        = {574--597},
 doi          = {10.1016/j.jsc.2010.01.009},
)
@inproceedings(Timbuk01,
 author       = {Thomas Genet and Val{\'{e}}rie Viet Triem Tong},
 year         = {2001},
 title        = {Reachability Analysis of Term Rewriting Systems with {Timbuk}},
 editor       = {Robert Nieuwenhuis and Andrei Voronkov},
 booktitle    = {Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
 series       = {Lecture Notes in Computer Science},
 volume       = {2250},
 publisher    = {Springer},
 pages        = {695--706},
 doi          = {10.1007/3-540-45653-8\_48},
)
@inproceedings(AProVE,
 author       = {J{\"{u}}rgen Giesl and Schneider{-}Kamp, Peter and Ren{\'{e}} Thiemann},
 year         = {2006},
 title        = {{AProVE 1.2}: Automatic Termination Proofs in the Dependency Pair Framework},
 booktitle    = {Proceedings of the 3rd International Joint Conference on Automated Reasoning},
 series       = {Lecture Notes in Computer Science},
 volume       = {4130},
 publisher    = {Springer},
 pages        = {281--286},
 doi          = {10.1007/11814771\_24},
)
@inproceedings(coscart-2015,
 author       = {Karl Gmeiner},
 year         = {2015},
 title        = {{CoScart}: Confluence Prover in {Scala}},
 booktitle    = {Proceedings of the 4th International Workshop on Confluence},
 pages        = {45},
)
@inproceedings(GN14wpte,
 author       = {Karl Gmeiner and Naoki Nishida},
 year         = {2014},
 title        = {Notes on Structure-Preserving Transformations of Conditional Term Rewrite Systems},
 booktitle    = {Proceedings of the first International Workshop on Rewriting Techniques for Program Transformations and Evaluation},
 series       = {OpenAccess Series in Informatics},
 volume       = {40},
 publisher    = {Schloss Dagstuhl -- Leibniz-Zentrum f\"ur Informatik},
 pages        = {3--14},
 doi          = {10.4230/OASIcs.WPTE.2014.3},
)
@inproceedings(GNG13iwc,
 author       = {Karl Gmeiner and Naoki Nishida and Bernhard Gramlich},
 year         = {2013},
 title        = {Proving Confluence of Conditional Term Rewriting Systems via Unravelings},
 booktitle    = {Proceedings of the 2nd International Workshop on Confluence},
 pages        = {35--39},
)
@inproceedings(GLR16,
 author       = {Ra\'ul Guti\'errez and Salvador Lucas and Patricio Reinoso},
 year         = {2016},
 title        = {A tool for the automatic generation of logical models of order-sorted first-order theories},
 booktitle    = {Proceedings of the XVI Jornadas sobre Programaci\'on y Lenguages},
 pages        = {215--230},
 note         = {Tool available at \url{http://zenon.dsic.upv.es/ages/}},
)
@inproceedings(HR89,
 author       = {Manuel V. Hermenegildo and Francesca Rossi},
 year         = {1989},
 title        = {On the Correctness and Efficiency of Independent And-Parallelism in Logic Programs},
 booktitle    = {Proceedings of the North American Conference on Logic Programming},
 publisher    = {{MIT} Press},
 pages        = {369--389},
)
@inproceedings(Hul80,
 author       = {Jean{-}Marie Hullot},
 year         = {1980},
 title        = {Canonical Forms and Unification},
 booktitle    = {Proceedings of the 5th Conference on Automated Deduction},
 series       = {Lecture Notes in Computer Science},
 volume       = {87},
 publisher    = {Springer},
 pages        = {318--334},
 doi          = {10.1007/3-540-10009-1\_25},
)
@inproceedings(Luc17lopstr,
 author       = {Salvador Lucas},
 year         = {2018},
 title        = {A Semantic Approach to the Analysis of Rewriting-Based Systems},
 booktitle    = {Revised Selected Papers of the 27th International Symposium on Logic-Based Program Synthesis and Transformation},
 series       = {Lecture Notes in Computer Science},
 volume       = {10855},
 publisher    = {Springer},
 pages        = {180--97},
 doi          = {10.1007/978-3-319-94460-9\_11},
)
@inproceedings(Luc17iwc,
 author       = {Salvador Lucas and Ra\'ul Guti\'errez},
 year         = {2017},
 title        = {A Semantic Criterion for Proving Infeasibility in Conditional Rewriting},
 booktitle    = {Proceedings of the 6th International Workshop on Confluence},
 pages        = {15--20},
)
@article(LMM05,
 author       = {Salvador Lucas and Claude March{\'{e}} and Jos{\'{e}} Meseguer},
 year         = {2005},
 title        = {Operational termination of conditional term rewriting systems},
 journal      = {Information Processing Letters},
 volume       = {95},
 number       = {4},
 pages        = {446--453},
 doi          = {10.1016/j.ipl.2005.05.002},
)
@inproceedings(Mar96,
 author       = {Massimo Marchiori},
 year         = {1996},
 title        = {Unravelings and Ultra-properties},
 booktitle    = {Proceedings of the 5th International Conference on Algebraic and Logic Programming},
 series       = {Lecture Notes in Computer Science},
 volume       = {1139},
 publisher    = {Springer},
 pages        = {107--121},
 doi          = {10.1007/3-540-61735-3\_7},
)
@article(MH94,
 author       = {Aart Middeldorp and Erik Hamoen},
 year         = {1994},
 title        = {Completeness Results for Basic Narrowing},
 journal      = {Applicable Algebra in Engineering, Communication and Computing},
 volume       = {5},
 pages        = {213--253},
 doi          = {10.1007/BF01190830},
)
@inproceedings(co3-2015,
 author       = {Naoki Nishida and Takayuki Kuroda and Makishi Yanagisawa and Karl Gmeiner},
 year         = {2015},
 title        = {{CO3: a COnverter for proving COnfluence of COnditional TRSs}},
 booktitle    = {Proceedings of the 4th International Workshop on Confluence},
 pages        = {42},
)
@inproceedings(NM18fscd,
 author       = {Naoki Nishida and Yuya Maeda},
 year         = {2018},
 title        = {Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems},
 booktitle    = {Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction},
 series       = {Leibniz International Proceedings in Informatics},
 volume       = {108},
 publisher    = {Schloss Dagstuhl -- Leibniz-Zentrum f\"ur Informatik},
 pages        = {26:1--26:20},
 doi          = {10.4230/LIPIcs.FSCD.2018.26},
)
@inproceedings(NV12lopstr,
 author       = {Naoki Nishida and Germ{\'{a}}n Vidal},
 year         = {2013},
 title        = {Computing More Specific Versions of Conditional Rewriting Systems},
 booktitle    = {Revised Selected Papers of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation},
 series       = {Lecture Notes in Computer Science},
 volume       = {7844},
 publisher    = {Springer},
 pages        = {137--154},
 doi          = {10.1007/978-3-642-38197-3\_10},
)
@inproceedings(NV13,
 author       = {Naoki Nishida and Germ{\'{a}}n Vidal},
 year         = {2014},
 title        = {A Finite Representation of the Narrowing Space},
 booktitle    = {Revised Selected Papers of the 23rd International Symposium on Logic-Based Program Synthesis and Transformation},
 series       = {Lecture Notes in Computer Science},
 volume       = {8901},
 publisher    = {Springer},
 pages        = {54--71},
 doi          = {10.1007/978-3-319-14125-1\_4},
)
@article(NV15,
 author       = {Naoki Nishida and Germ{\'{a}}n Vidal},
 year         = {2015},
 title        = {A framework for computing finite {SLD} trees},
 journal      = {Journal of Logic and Algebraic Methods in Programming},
 volume       = {84},
 number       = {2},
 pages        = {197--217},
 doi          = {10.1016/j.jlamp.2014.11.006},
)
@book(Ohl02,
 author       = {Enno Ohlebusch},
 year         = {2002},
 title        = {Advanced Topics in Term Rewriting},
 publisher    = {Springer},
 doi          = {10.1007/978-1-4757-3661-8},
)
@inproceedings(Pal90,
 author       = {Catuscia Palamidessi},
 year         = {1990},
 title        = {Algebraic Properties of Idempotent Substitutions},
 booktitle    = {Proceedings of the 17th International Colloquium on Automata, Languages and Programming},
 series       = {Lecture Notes in Computer Science},
 volume       = {443},
 publisher    = {Springer},
 pages        = {386--399},
 doi          = {10.1007/BFb0032046},
)
@article(Sla74,
 author       = {James R. Slagle},
 year         = {1974},
 title        = {Automated Theorem-Proving for Theories with Simplifiers, Commutativity and Associativity},
 journal      = {Journal of the ACM},
 volume       = {21},
 number       = {4},
 pages        = {622--642},
 doi          = {10.1145/321850.321859},
)
@inproceedings(concon-2014,
 author       = {Thomas Sternagel and Aart Middeldorp},
 year         = {2014},
 title        = {Conditional Confluence (System Description)},
 booktitle    = {Proceedings of the Joint International Conference on Rewriting and Typed Lambda Calculi},
 series       = {Lecture Notes in Computer Science},
 volume       = {8560},
 publisher    = {Springer},
 pages        = {456--465},
 doi          = {10.1007/978-3-319-08918-8\_31},
)
@inproceedings(SMI95,
 author       = {Taro Suzuki and Aart Middeldorp and Tetsuo Ida},
 year         = {1995},
 title        = {Level-Confluence of Conditional Rewrite Systems with Extra Variables in Right-Hand Sides},
 booktitle    = {Proceedings of the 6th International Conference on Rewriting Techniques and Applications},
 series       = {Lecture Notes in Computer Science},
 volume       = {914},
 publisher    = {Springer},
 pages        = {179--193},
 doi          = {10.1007/3-540-59200-8\_56},
)