| Publication | Date of Publication | Type |
|---|
| Formalizing almost development closed critical pairs (short paper) | 2024-11-26 | Paper |
| Hydra battles and AC termination | 2024-10-21 | Paper |
| Polynomial termination over \(\mathbb{N}\) is undecidable | 2024-05-27 | Paper |
| Left-Linear Completion with AC Axioms | 2024-04-26 | Paper |
| Confluence Criteria for Logically Constrained Rewrite Systems | 2024-04-26 | Paper |
| First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification | 2023-06-27 | Paper |
| Completeness of combinations of conditional constructor systems | 2023-03-09 | Paper |
| Confluence of the disjoint union of conditional term rewriting systems | 2023-03-09 | Paper |
| Modular aspects of properties of term rewriting systems related to normal forms | 2022-12-09 | Paper |
| Completeness of combinations of constructor systems | 2022-12-09 | Paper |
| Level-confluence of conditional rewrite systems with extra variables in right-hand sides | 2022-12-09 | Paper |
| Lazy narrowing: strong completeness and eager variable elimination (extended abstract) | 2022-08-18 | Paper |
| Formalized proofs of the infinity and normal form predicates in the first-order theory of rewriting | 2021-11-10 | Paper |
| Certifying proofs in the first-order theory of rewriting | 2021-10-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4993364 | 2021-06-15 | Paper |
| Completion for logically constrained rewriting | 2021-06-15 | Paper |
| ProTeM: a proof term manipulator (system description) | 2021-06-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5111315 | 2020-05-26 | Paper |
| Composing proof terms | 2020-03-10 | Paper |
| Simple termination revisited | 2020-01-21 | Paper |
| Decidable call by need computations in term rewriting (extended abstract) | 2019-10-01 | Paper |
| Abstract completion, formalized | 2019-09-13 | Paper |
| Transforming termination by self-labelling | 2019-01-15 | Paper |
| FORT 2.0 | 2018-10-18 | Paper |
| AC-KBO revisited | 2017-11-09 | Paper |
| Constructing cycles in the simplex method for DPLL(T) | 2017-11-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5369502 | 2017-10-17 | Paper |
| CSI: new evidence -- a progress report | 2017-09-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5277883 | 2017-07-12 | Paper |
| Conditional complexity | 2017-07-12 | Paper |
| Leftmost outermost revisited | 2017-07-12 | Paper |
| Complexity of conditional term rewriting | 2017-05-08 | Paper |
| Normalized completion revisited | 2017-02-01 | Paper |
| Beyond Peano arithmetic -- automatically proving termination of the Goodstein sequence | 2017-02-01 | Paper |
| Certification of classical confluence results for left-linear term rewrite systems | 2016-10-27 | Paper |
| Strongly sequential and inductively sequential term rewriting systems | 2016-06-09 | Paper |
| Layer systems for proving confluence | 2015-09-17 | Paper |
| Labelings for decreasing diagrams | 2015-07-02 | Paper |
| Transforming SAT into termination of rewriting | 2015-04-09 | Paper |
| Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations | 2015-01-14 | Paper |
| Polynomial interpretations over the natural, rational and real numbers revisited | 2014-09-30 | Paper |
| A New and Formalized Proof of Abstract Completion | 2014-09-08 | Paper |
| AC-KBO revisited | 2014-07-24 | Paper |
| Conditional confluence (system description) | 2014-07-24 | Paper |
| Innermost termination of rewrite systems by labeling | 2014-01-24 | Paper |
| Approximations for strategies and termination | 2013-08-23 | Paper |
| Uncurrying for termination and complexity | 2013-07-05 | Paper |
| Multi-completion with termination tools | 2013-07-05 | Paper |
| Layer systems for proving confluence | 2012-08-31 | Paper |
| Decreasing diagrams and relative termination | 2012-07-31 | Paper |
| Ordinals and Knuth-Bendix orders | 2012-06-15 | Paper |
| On the domain and dimension hierarchy of matrix interpretations | 2012-06-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5389156 | 2012-04-25 | Paper |
| Polynomial interpretations over the reals do not subsume polynomial interpretations over the integers | 2012-04-25 | Paper |
| Labelings for Decreasing Diagrams. | 2012-04-24 | Paper |
| Revisiting matrix interpretations for proving termination of term rewriting | 2012-04-24 | Paper |
| AC completion with termination tools | 2011-07-29 | Paper |
| CSI -- a confluence tool | 2011-07-29 | Paper |
| Joint spectral radius theory for automated complexity analysis of rewrite systems | 2011-07-08 | Paper |
| Satisfiability of non-linear (ir)rational arithmetic | 2011-01-07 | Paper |
| Revisiting matrix interpretations for polynomial derivational complexity of term rewriting | 2010-10-12 | Paper |
| Termination tools in ordered completion | 2010-09-14 | Paper |
| Decreasing diagrams and relative termination | 2010-09-14 | Paper |
| Monotonicity criteria for polynomial interpretations over the naturals | 2010-09-14 | Paper |
| Automating the dependency pair method. | 2010-04-20 | Paper |
| KBO orientability | 2010-02-01 | Paper |
| Finding and certifying loops | 2010-01-28 | Paper |
| Increasing interpretations | 2009-12-11 | Paper |
| Match-bounds revisited | 2009-11-27 | Paper |
| Beyond Dependency Graphs | 2009-07-28 | Paper |
| Rewriting Techniques and Applications | 2009-04-30 | Paper |
| SAT Solving for Termination Analysis with Polynomial Interpretations | 2009-03-10 | Paper |
| Predictive Labeling with Dependency Pairs Using SAT | 2009-03-06 | Paper |
| Uncurrying for Termination | 2009-01-27 | Paper |
| Increasing Interpretations | 2009-01-27 | Paper |
| Multi-completion with Termination Tools (System Description) | 2008-11-27 | Paper |
| Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems | 2008-11-20 | Paper |
| Predictive Labeling | 2008-09-25 | Paper |
| Root-Labeling | 2008-08-28 | Paper |
| Maximal Termination | 2008-08-28 | Paper |
| Constraints for Argument Filterings | 2008-03-07 | Paper |
| Proving Termination of Rewrite Systems Using Bounds | 2008-01-02 | Paper |
| Satisfying KBO Constraints | 2008-01-02 | Paper |
| Tyrolean termination tool: techniques and features | 2007-04-16 | Paper |
| Term Rewriting and Applications | 2005-11-11 | Paper |
| Transformation techniques for context-sensitive rewrite systems | 2005-09-27 | Paper |
| Artificial Intelligence and Symbolic Computation | 2005-08-19 | Paper |
| Automating the dependency pair method | 2005-08-05 | Paper |
| Decidable call-by-need computations in term rewriting | 2005-02-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4447241 | 2004-02-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4413068 | 2003-07-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4412115 | 2003-07-13 | Paper |
| Relative undecidability in term rewriting. I: The termination hierarchy | 2003-01-14 | Paper |
| Relative undecidability in term rewriting. II: The confluence hierarchy | 2003-01-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4548266 | 2002-08-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4539643 | 2002-07-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4537513 | 2002-07-01 | Paper |
| A deterministic lazy narrowing calculus | 2002-04-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2769431 | 2002-02-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2763640 | 2002-01-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2753692 | 2001-11-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2723429 | 2001-07-05 | Paper |
| Type introduction for equational rewriting | 2000-11-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4503959 | 2000-09-14 | Paper |
| Completeness of combinations of conditional constructor systems | 2000-08-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4705617 | 1999-12-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4705614 | 1999-12-20 | Paper |
| Simple termination of rewrite systems | 1998-07-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4376069 | 1998-06-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4362915 | 1998-04-01 | Paper |
| A sequential reduction strategy | 1997-02-27 | Paper |
| Lazy narrowing: strong completeness and eager variable elimination | 1997-02-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4834485 | 1995-05-30 | Paper |
| Simple termination is difficult | 1995-01-31 | Paper |
| Modular properties of conditional term rewriting systems | 1994-09-06 | Paper |
| Completeness results for basic narrowing | 1994-07-04 | Paper |
| Modularity of confluence: A simplified proof | 1994-04-04 | Paper |
| Completeness of combinations of constructor systems | 1993-08-22 | Paper |
| Sequentiality in orthogonal term rewriting systems | 1992-06-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3204048 | 1989-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3806800 | 1988-01-01 | Paper |
