P. Aczel. Schematic Consequence. In D. Gabbay, editor, What is a Logical System, pages 261--272, Oxford University Press, 1994.
B. Alarcón, F. Emmes, C. Fuhs, J. Giesl, R. Gutiérrez, S. Lucas, P. Schneider-Kamp, and R. Thiemann. Improving Context-Sensitive Dependency Pairs. In Proc. of LPAR'08, LNCS 5330:636--651, 2008.
B. Alarcón, S. Lucas, and J. Meseguer. A Dependency Pair Framework for A∨C-Termination. In Proc. of WRLA'10, LNCS 6381:35--51, 2010.
[+]
P. Aczel. Schematic Consequence. In D. Gabbay, editor, What is a Logical System, pages 261--272, Oxford University Press, 1994.
B. Alarcón, F. Emmes, C. Fuhs, J. Giesl, R. Gutiérrez, S. Lucas, P. Schneider-Kamp, and R. Thiemann. Improving Context-Sensitive Dependency Pairs. In Proc. of LPAR'08, LNCS 5330:636--651, 2008.
B. Alarcón, S. Lucas, and J. Meseguer. A Dependency Pair Framework for A∨C-Termination. In Proc. of WRLA'10, LNCS 6381:35--51, 2010.
H.P. Barendregt, W. Dekkers, and R. Statman. Lambda Calculus with Types. Cambridge University Press, 2013.
M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. Talcott. All About Maude -- A High-Performance Logical Framework, LNCS volume 4350, 2007.
M. Codish and C. Taboch. A semantic basis for the termination analysis of logic programs. Journal of Logic Programming 41:103--123, 1999.
N. Dershowitz, N. Lindenstrauss, Y. Sagiv, and A. Serebrenik. A General Framework for Automatic Termination of Logic Programs. Applicable Algebra in Engineering, Communication and Computing, 12:117--156, 2001.
N. Dershowitz and Z. Manna. Proving Termination with Multiset Orderings. Communications of the ACM 22(8):465--476, 1979.
F. Durán, S. Lucas, J. Meseguer, C. Marché, and X. Urbain. Proving Termination of Membership Equational Programs. In Proc. of PEPM'04, pages 147--158, ACM Press, New York, 2004.
F. Durán, S. Lucas, C. Marché, J. Meseguer, X. Urbain, Proving Operational Termination of Membership Equational Programs, Higher-Order and Symbolic Computation 21(1-2):59--88, 2008.
F. Durán, S. Lucas, J. Meseguer. Methods for Proving Termination of Rewriting-based Programming Languages by Transformation. Electronic Notes in Theoretical Computer Science, 248:93--113, 2009.
F. Durán, S. Lucas, and J. Meseguer. MTT: The Maude Termination Tool (System Description). Proc. of IJCAR'08. LNAI 5195:313--319, 2008.
S. Falke and D. Kapur. Dependency Pairs for Rewriting with Built-in Numbers and Semantic Data Structures. In Proc. of RTA'08, LNCS 5117:94--109, 2008.
J. Giesl and D. Kapur. Dependency Pairs for Equational Rewriting. Proc. of RTA'01, LNCS 2051:93--108, 2001.
J. Giesl, R. Thiemann, and P. Schneider-Kamp. The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs. In Proc. of LPAR'04, LNAI 3452:301--331, 2004.
J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Mechanizing and Improving Dependency Pairs. Journal of Automatic Reasoning, 37(3):155--203, 2006.
R. Gutiérrez and S. Lucas. Proving Termination in the Context-Sensitive Depedency Pairs Framework. In Proc of WRLA'10 LNCS 6381:19--35, 2010.
S. Lucas. Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming, 1998(1):1--61, January 1998.
S. Lucas. Context-sensitive rewriting strategies. Information and Computation, 178(1):294--343, 2002.
S. Lucas and J. Meseguer. 2D Dependency Pairs for Proving Operational Termination of CTRSs. In Proc. of WRLA'14, LNCS vol. 8663, to appear, 2014.
S. Lucas and J. Meseguer. Order-Sorted Dependency Pairs. In Proc. of PPDP'08, pages 108--119, ACM Press, 2008.
S. Lucas, C. Marché, and J. Meseguer. Operational termination of conditional term rewriting systems. Information Processing Letters, 95:446--453, 2005.
J. Meseguer. General Logics. In H.-D. Ebbinghaus et al., editors, Logic Colloquium'87, pages 275--329, North-Holland, 1989.
J. Meseguer. Membership algebra as a logical framework for equational specification. In Proc. of WADT'97, LNCS 1376:18--61, 1998.
M. Nakamura, K. Ogata, and K. Futatsugi. On Proving Operational Termination Incrementally with Modular Conditional Dependency Pairs. International Journal of Computer Science, 40:2, 2013.
M.T. Nguyen, J. Giesl, P. Schneider-Kamp, and D. De Schreye. Termination Analysis of Logic Programs Based on Dependency Graphs. In Proc. of LOPSTR 2007, LNCS 4915:8--22, 2007.
E. Ohlebusch. Advanced Topics in Term Rewriting. Springer-Verlag, 2002.
F. Schernhammer and B. Gramlich. Characterizing and proving operational termination of deterministic conditional term rewriting systems. Journal of Logic and Algebraic Programming 79:659--688, 2010.
D. de Scheye and S. Decorte. Termination of Logic Programs: The Never-Ending Story. Journal of Logic Programming, 19:199--260, 1994.
P. Schneider-Kamp, J. Giesl, and M.T. Nguyen. The Dependency Triple Framework for Termination of Logic Programs. In Proc. of LOPSTR 2009, LNCS 6037:37--51, 2009.
[-]