| 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
Journal of Automated Reasoning | 2023-06-27 | Paper |
Completeness of combinations of conditional constructor systems
Conditional Term Rewriting Systems | 2023-03-09 | Paper |
Confluence of the disjoint union of conditional term rewriting systems
Conditional and Typed Rewriting Systems | 2023-03-09 | Paper |
Modular aspects of properties of term rewriting systems related to normal forms
Rewriting Techniques and Applications | 2022-12-09 | Paper |
Completeness of combinations of constructor systems
Rewriting Techniques and Applications | 2022-12-09 | Paper |
Level-confluence of conditional rewrite systems with extra variables in right-hand sides
Rewriting Techniques and Applications | 2022-12-09 | Paper |
Lazy narrowing: strong completeness and eager variable elimination (extended abstract)
TAPSOFT '95: Theory and Practice of Software Development | 2022-08-18 | Paper |
Formalized proofs of the infinity and normal form predicates in the first-order theory of rewriting
Tools and Algorithms for the Construction and Analysis of Systems | 2021-11-10 | Paper |
Certifying proofs in the first-order theory of rewriting
| 2021-10-18 | Paper |
scientific article; zbMATH DE number 7359428 (Why is no real title available?)
| 2021-06-15 | Paper |
Completion for logically constrained rewriting
| 2021-06-15 | Paper |
ProTeM: a proof term manipulator (system description)
| 2021-06-15 | Paper |
scientific article; zbMATH DE number 7204438 (Why is no real title available?)
| 2020-05-26 | Paper |
Composing proof terms
| 2020-03-10 | Paper |
Simple termination revisited
Automated Deduction — CADE-12 | 2020-01-21 | Paper |
Decidable call by need computations in term rewriting (extended abstract)
Automated Deduction—CADE-14 | 2019-10-01 | Paper |
Abstract completion, formalized
| 2019-09-13 | Paper |
Transforming termination by self-labelling
Automated Deduction — Cade-13 | 2019-01-15 | Paper |
FORT 2.0
| 2018-10-18 | Paper |
AC-KBO revisited
Theory and Practice of Logic Programming | 2017-11-09 | Paper |
Constructing cycles in the simplex method for DPLL(T)
| 2017-11-03 | Paper |
scientific article; zbMATH DE number 6792369 (Why is no real title available?)
| 2017-10-17 | Paper |
CSI: new evidence -- a progress report
| 2017-09-22 | Paper |
scientific article; zbMATH DE number 6744203 (Why is no real title available?)
| 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
Interactive Theorem Proving | 2016-10-27 | Paper |
Strongly sequential and inductively sequential term rewriting systems
Information Processing Letters | 2016-06-09 | Paper |
Layer systems for proving confluence
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Labelings for decreasing diagrams
Journal of Automated Reasoning | 2015-07-02 | Paper |
Transforming SAT into termination of rewriting
Electronic Notes in Theoretical Computer Science | 2015-04-09 | Paper |
Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations
Journal of Symbolic Computation | 2015-01-14 | Paper |
Polynomial interpretations over the natural, rational and real numbers revisited
Logical Methods in Computer Science | 2014-09-30 | Paper |
A New and Formalized Proof of Abstract Completion
Interactive Theorem Proving | 2014-09-08 | Paper |
AC-KBO revisited
Functional and Logic Programming | 2014-07-24 | Paper |
Conditional confluence (system description)
Lecture Notes in Computer Science | 2014-07-24 | Paper |
Innermost termination of rewrite systems by labeling
Electronic Notes in Theoretical Computer Science | 2014-01-24 | Paper |
Approximations for strategies and termination
| 2013-08-23 | Paper |
Uncurrying for termination and complexity
Journal of Automated Reasoning | 2013-07-05 | Paper |
Multi-completion with termination tools
Journal of Automated Reasoning | 2013-07-05 | Paper |
Layer systems for proving confluence
| 2012-08-31 | Paper |
Decreasing diagrams and relative termination
Journal of Automated Reasoning | 2012-07-31 | Paper |
Ordinals and Knuth-Bendix orders
Logic for Programming, Artificial Intelligence, and Reasoning | 2012-06-15 | Paper |
On the domain and dimension hierarchy of matrix interpretations
Logic for Programming, Artificial Intelligence, and Reasoning | 2012-06-15 | Paper |
scientific article; zbMATH DE number 6027911 (Why is no real title available?)
| 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
Lecture Notes in Computer Science | 2011-07-29 | Paper |
CSI -- a confluence tool
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Joint spectral radius theory for automated complexity analysis of rewrite systems
Algebraic Informatics | 2011-07-08 | Paper |
Satisfiability of non-linear (ir)rational arithmetic
Logic for Programming, Artificial Intelligence, and Reasoning | 2011-01-07 | Paper |
Revisiting matrix interpretations for polynomial derivational complexity of term rewriting
Logic for Programming, Artificial Intelligence, and Reasoning | 2010-10-12 | Paper |
Termination tools in ordered completion
Automated Reasoning | 2010-09-14 | Paper |
Decreasing diagrams and relative termination
Automated Reasoning | 2010-09-14 | Paper |
Monotonicity criteria for polynomial interpretations over the naturals
Automated Reasoning | 2010-09-14 | Paper |
Automating the dependency pair method.
Lecture Notes in Computer Science | 2010-04-20 | Paper |
KBO orientability
Journal of Automated Reasoning | 2010-02-01 | Paper |
Finding and certifying loops
SOFSEM 2010: Theory and Practice of Computer Science | 2010-01-28 | Paper |
Increasing interpretations
Annals of Mathematics and Artificial Intelligence | 2009-12-11 | Paper |
Match-bounds revisited
Information and Computation | 2009-11-27 | Paper |
Beyond Dependency Graphs
Automated Deduction – CADE-22 | 2009-07-28 | Paper |
Rewriting Techniques and Applications
Lecture Notes in Computer Science | 2009-04-30 | Paper |
SAT Solving for Termination Analysis with Polynomial Interpretations
Theory and Applications of Satisfiability Testing – SAT 2007 | 2009-03-10 | Paper |
Predictive Labeling with Dependency Pairs Using SAT
Automated Deduction – CADE-21 | 2009-03-06 | Paper |
Uncurrying for Termination
Logic for Programming, Artificial Intelligence, and Reasoning | 2009-01-27 | Paper |
Increasing Interpretations
Lecture Notes in Computer Science | 2009-01-27 | Paper |
Multi-completion with Termination Tools (System Description)
Automated Reasoning | 2008-11-27 | Paper |
Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems
Language and Automata Theory and Applications | 2008-11-20 | Paper |
Predictive Labeling
Lecture Notes in Computer Science | 2008-09-25 | Paper |
Root-Labeling
Rewriting Techniques and Applications | 2008-08-28 | Paper |
Maximal Termination
Rewriting Techniques and Applications | 2008-08-28 | Paper |
Constraints for Argument Filterings
Lecture Notes in Computer Science | 2008-03-07 | Paper |
Proving Termination of Rewrite Systems Using Bounds
Lecture Notes in Computer Science | 2008-01-02 | Paper |
Satisfying KBO Constraints
Lecture Notes in Computer Science | 2008-01-02 | Paper |
Tyrolean termination tool: techniques and features
Information and Computation | 2007-04-16 | Paper |
Term Rewriting and Applications
Lecture Notes in Computer Science | 2005-11-11 | Paper |
Transformation techniques for context-sensitive rewrite systems
Journal of Functional Programming | 2005-09-27 | Paper |
Artificial Intelligence and Symbolic Computation
Lecture Notes in Computer Science | 2005-08-19 | Paper |
Automating the dependency pair method
Information and Computation | 2005-08-05 | Paper |
Decidable call-by-need computations in term rewriting
Information and Computation | 2005-02-22 | Paper |
scientific article; zbMATH DE number 2043537 (Why is no real title available?)
| 2004-02-16 | Paper |
scientific article; zbMATH DE number 1950452 (Why is no real title available?)
| 2003-07-17 | Paper |
scientific article; zbMATH DE number 1948501 (Why is no real title available?)
| 2003-07-13 | Paper |
Relative undecidability in term rewriting. I: The termination hierarchy
Information and Computation | 2003-01-14 | Paper |
Relative undecidability in term rewriting. II: The confluence hierarchy
Information and Computation | 2003-01-14 | Paper |
scientific article; zbMATH DE number 1788632 (Why is no real title available?)
| 2002-08-26 | Paper |
scientific article; zbMATH DE number 1765702 (Why is no real title available?)
| 2002-07-10 | Paper |
scientific article; zbMATH DE number 1761894 (Why is no real title available?)
| 2002-07-01 | Paper |
A deterministic lazy narrowing calculus
Journal of Symbolic Computation | 2002-04-29 | Paper |
scientific article; zbMATH DE number 1701352 (Why is no real title available?)
| 2002-02-05 | Paper |
scientific article; zbMATH DE number 1692899 (Why is no real title available?)
| 2002-01-21 | Paper |
scientific article; zbMATH DE number 1670496 (Why is no real title available?)
| 2001-11-11 | Paper |
scientific article; zbMATH DE number 1614705 (Why is no real title available?)
| 2001-07-05 | Paper |
Type introduction for equational rewriting
Acta Informatica | 2000-11-22 | Paper |
scientific article; zbMATH DE number 1507237 (Why is no real title available?)
| 2000-09-14 | Paper |
Completeness of combinations of conditional constructor systems
Journal of Symbolic Computation | 2000-08-14 | Paper |
scientific article; zbMATH DE number 1380897 (Why is no real title available?)
| 1999-12-20 | Paper |
scientific article; zbMATH DE number 1380895 (Why is no real title available?)
| 1999-12-20 | Paper |
Simple termination of rewrite systems
Theoretical Computer Science | 1998-07-23 | Paper |
scientific article; zbMATH DE number 1114350 (Why is no real title available?)
| 1998-06-11 | Paper |
scientific article; zbMATH DE number 1086665 (Why is no real title available?)
| 1998-04-01 | Paper |
A sequential reduction strategy
Theoretical Computer Science | 1997-02-27 | Paper |
Lazy narrowing: strong completeness and eager variable elimination
Theoretical Computer Science | 1997-02-27 | Paper |
scientific article; zbMATH DE number 759443 (Why is no real title available?)
| 1995-05-30 | Paper |
Simple termination is difficult
Applicable Algebra in Engineering, Communication and Computing | 1995-01-31 | Paper |
Modular properties of conditional term rewriting systems
Information and Computation | 1994-09-06 | Paper |
Completeness results for basic narrowing
Applicable Algebra in Engineering, Communication and Computing | 1994-07-04 | Paper |
Modularity of confluence: A simplified proof
Information Processing Letters | 1994-04-04 | Paper |
Completeness of combinations of constructor systems
Journal of Symbolic Computation | 1993-08-22 | Paper |
Sequentiality in orthogonal term rewriting systems
Journal of Symbolic Computation | 1992-06-28 | Paper |
scientific article; zbMATH DE number 4180808 (Why is no real title available?)
| 1989-01-01 | Paper |
scientific article; zbMATH DE number 4076598 (Why is no real title available?)
| 1988-01-01 | Paper |
