| Improving Rewriting Induction Approach for Proving Ground Confluence. | 0 | 0.34 | 2017 |
| Parallel Closure Theorem for Left-Linear Nominal Rewriting Systems. | 0 | 0.34 | 2017 |
| Critical Pair Analysis in Nominal Rewriting. | 2 | 0.39 | 2016 |
| Normalisation by Random Descent. | 0 | 0.34 | 2016 |
| Ground Confluence Prover based on Rewriting Induction. | 1 | 0.35 | 2016 |
| Confluence of Orthogonal Nominal Rewriting Systems Revisited. | 5 | 0.55 | 2015 |
| Correctness of Context-Moving Transformations for Term Rewriting Systems. | 0 | 0.34 | 2015 |
| Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams. | 0 | 0.34 | 2014 |
| A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems | 9 | 0.58 | 2011 |
| Program Transformation Templates For Tupling Based On Term Rewriting | 1 | 0.35 | 2010 |
| Proving Confluence of Term Rewriting Systems Automatically | 24 | 1.23 | 2009 |
| Termination Proof of S-Expression Rewriting Systems with Recursive Path Relations | 2 | 0.36 | 2008 |
| Modular Church-Rosser Modulo: The Complete Picture | 4 | 0.43 | 2008 |
| Elimination Transformations for Associative---Commutative Rewriting Systems | 4 | 0.45 | 2006 |
| Reduction strategies for left-linear term rewriting systems | 1 | 0.36 | 2005 |
| Confluent term rewriting systems | 3 | 0.41 | 2005 |
| Program transformation by templates based on term rewriting | 7 | 0.45 | 2005 |
| Termination of S-Expression Rewriting Systems: Lexicographic Path Ordering for Higher-Order Terms | 7 | 0.52 | 2004 |
| Inductive Theorems for Higher-Order Rewriting | 4 | 0.45 | 2004 |
| New Challenges for Compuational Models | 0 | 0.34 | 2000 |
| Argument Filtering Transformation | 50 | 2.04 | 1999 |
| Decidability for Left-Linear Growing Term Rewriting Systems | 37 | 1.45 | 1999 |
| Termination Transformation by Tree Lifting Ordering | 1 | 0.36 | 1998 |
| Persistency of Confluence | 12 | 0.64 | 1997 |
| On Composable Properties of Term Rewriting Systems | 3 | 0.45 | 1997 |
| Semantics and strong sequentiality of priority term rewriting systems | 2 | 0.36 | 1996 |
| Church-Rosser Property and Unique Normal Form Property of Non-Duplicating Term Rewriting Systems | 13 | 0.83 | 1994 |
| Modularity of confluence: a simplified proof | 20 | 1.06 | 1994 |
| How to prove equivalence of term rewriting systems without induction | 9 | 0.79 | 1991 |
| Completeness of combinations of constructor systems | 49 | 2.89 | 1991 |
| Termination for the Direct Sum of left-Linear Term Rewriting Systems -Preliminary Draft- | 29 | 2.92 | 1989 |
| Fast Knuth-Bendix completion with a term rewriting system compiler | 2 | 0.90 | 1989 |
| On the Church-Rosser property for the direct sum of term rewriting systems | 108 | 14.10 | 1987 |
| Counterexamples to termination for the direct sum of term rewriting systems | 123 | 11.50 | 1987 |
| On Equivalence Transformations for Term Rewriting Systems | 1 | 0.39 | 1984 |
