Loop detection in term rewriting using the eliminating unfoldings

Alpuente, 2003, Abstract diagnosis of functional programs, vol. 2664, 1

Alpuente, 1995, Analyses of unsatisfiability for equational logic programming, Journal of Logic Programming, 311, 479

Alpuente, 1997, Safe folding/unfolding with conditional narrowing, vol. 1298, 1

Alpuente, 2004, Rules + strategies for transforming lazy functional logic programs, Theoretical Computer Science, 311, 479, 10.1016/j.tcs.2003.10.033

Alpuente, 1993, Narrowing approximations as an optimization for equational logic programs, vol. 714, 391

AProVE’s web site. http://aprove.informatik.rwth-aachen.de/

Arts, 2000, Termination of term rewriting using dependency pairs, Theoretical Computer Science, 236, 133, 10.1016/S0304-3975(99)00207-8

Franz Baader, Tobias Nipkow, Term rewriting and all that, Cambridge, 1998

Burstall, 1977, A transformation system for developing recursive programs, Journal of the ACM, 24, 44, 10.1145/321992.321996

Chabin, 1991, Narrowing directed by a graph of terms, vol. 488, 112

Codish, 1999, A semantics basis for termination analysis of logic programs, Journal of Logic Programming, 41, 103, 10.1016/S0743-1066(99)00006-0

Cousot, 1977, Abstract interpretation: A unifed lattice model for static analysis of programs by construction or approximation of fixpoints, 238

Cousot, 1978, Automatic discovery of linear restraints among variables of a program, 84

Dershowitz, 1981, Termination of linear rewriting systems, vol. 115, 448

Dershowitz, 1987, Termination of rewriting, Journal of Symbolic Computation, 3, 69, 10.1016/S0747-7171(87)80022-6

Drosten, 1989

Eén, 2004, An extensible SAT-solver, vol. 2919, 502

Gabbrielli, 1994, Goal independency and call patterns in the analysis of logic programs, 394

Genaim, 2001, Inferring termination condition for logic programs using backwards analysis, vol. 2250, 685

Alfons Geser, Dieter Hofbauer, Johannes Waldmann, Deciding termination for ancestor match-bounded string rewriting systems, Technical Report, National Institute of Aerospace, Hampton, VA, 2004

Geser, 1999, Non-looping string rewriting, RAIRO Theoretical Informatics and Applications, 33, 279, 10.1051/ita:1999118

Giesl, 2006, AProVE 1.2: Automatic termination proofs in the dependency pair framework, vol. 4130, 281

Giesl, 2004, The dependency pair framework: Combining techniques for automated termination proofs, vol. 3452, 210

Giesl, 2005, Proving and disproving termination of higher-order functions, vol. 3717, 216

Giesl, 2004, Automated termination proofs with AProVE, vol. 3091, 210

Guttag, 1983, On proving uniform termination and restricted termination of rewriting systems, SIAM Journal of Computing, 12, 189, 10.1137/0212012

Hanus, 1994, The integration of functions into logic programming: From theory to practice, Journal of Logic Programming, 19–20, 583, 10.1016/0743-1066(94)90034-5

Hirokawa, 2007, Tyrolean termination tool: Techniques and features, Information and Computation, 205, 474, 10.1016/j.ic.2006.08.010

Hölldobler, 1989, vol. 353

Kapur, 1991, Semi-unification, Theoretical Computer Science, 81, 169, 10.1016/0304-3975(91)90189-9

Winfried Kurth, Termination und konfluenz von semi-Thue-systemen mit nur einer regel, Ph.D. Thesis, Technische Universität Clausthal, Germany, 1990

D.S. Lankford, David R. Musser, A finite termination criterion, Unpublished Draft, USC Information Sciences Institute, Marina Del Rey, CA, 1978

Marché, 2007, The termination competition, vol. 4533, 303

Matchbox’s web site. http://dfa.imn.htwk-leipzig.de/matchbox/

Mesnard, 2005, cTI: A constraint-based termination inference tool for iso-prolog, Theory and Practice of Logic Programming, 5, 243, 10.1017/S1471068404002017

Payet, 2007, Detecting non-termination of term rewriting systems using an unfolding operator, vol. 4407, 194

Payet, 2004, Non-termination inference for constraint logic programs, vol. 3148, 377

Payet, 2006, Non-termination inference of logic programs, ACM Transactions on Programming Languages and Systems, 28, 256, 10.1145/1119479.1119481

Pettorossi, 1996, Rules and strategies for transforming functional and logic programs, ACM Computing Surveys, 28, 360, 10.1145/234528.234529

Schmidt, 2007, A calculus of logical relations for over- and underapproximating static analyses, Science of Computer Programming, 64, 29, 10.1016/j.scico.2006.03.008

Steinbach, 1995, Simplification orderings: History of results, Fundamenta Informaticae, 24, 47, 10.3233/FI-1995-24123

Tarski, 1955, A lattice theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, 5, 285, 10.2140/pjm.1955.5.285

Toyama, 1987, Counterexamples to the termination for the direct sum of term rewriting systems, Information Processing Letters, 25, 141, 10.1016/0020-0190(87)90122-0

TTT2’s web site. http://colo6-c703.uibk.ac.at/ttt2

Waldmann, 2004, Matchbox: A tool for match-bounded string rewriting, vol. 3091, 85

Johannes Waldmann, Compressed loops (draft). Available at: http://dfa.imn.htwk-leipzig.de/matchbox/methods/, 2007

Harald Zankl, Aart Middeldorp, Nontermination of string rewriting using SAT, in: Proc. of the 9th International Workshop on Termination, WST’07, 2007, pp. 52–55

Zantema, 2005, Termination of string rewriting proved automatically, Journal of Automated Reasoning, 34, 105, 10.1007/s10817-005-6545-0