Aart Middeldorp

CoRR, May, 2025

Automated Analysis of Logically Constrained Rewrite Systems using crest.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2025

Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems.

[BibT_eX]

[DOI]

Christina Kirk

Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2025

The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting.

[BibT_eX]

[DOI]

Johannes Niederhauser

Proceedings of the Automated Deduction - CADE 30, 2025

2024

Undecidability Results on Orienting Single Rewrite Rules.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2024

Linear Termination is Undecidable.

[BibT_eX]

[DOI]

Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, 2024

Confluence of Logically Constrained Rewrite Systems Revisited.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 12th International Joint Conference, 2024

2023

First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification.

[BibT_eX]

[DOI]

Alexander Lochmann

J. Autom. Reason., June, 2023

Confluence Criteria for Logically Constrained Rewrite Systems (Full Version).

[BibT_eX]

[DOI]

CoRR, 2023

Linear Termination over N is Undecidable.

[BibT_eX]

[DOI]

CoRR, 2023

Hydra Battles and AC Termination, Revisited.

[BibT_eX]

[DOI]

CoRR, 2023

Formalizing Almost Development Closed Critical Pairs (Short Paper).

[BibT_eX]

[DOI]

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

Hydra Battles and AC Termination.

[BibT_eX]

[DOI]

Proceedings of the 8th International Conference on Formal Structures for Computation and Deduction, 2023

A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems.

[BibT_eX]

[DOI]

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

Confluence Criteria for Logically Constrained Rewrite Systems.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 29, 2023

Left-Linear Completion with AC Axioms.

[BibT_eX]

[DOI]

Johannes Niederhauser

Proceedings of the Automated Deduction - CADE 29, 2023

2022

Polynomial Termination Over ℕ Is Undecidable.

[BibT_eX]

[DOI]

Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, 2022

2021

CoCo 2019: report on the eighth confluence competition.

[BibT_eX]

[DOI]

Kiraku Shintani

Int. J. Softw. Tools Technol. Transf., 2021

Certifying Proofs in the First-Order Theory of Rewriting.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems.

[BibT_eX]

[DOI]

Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

2020

Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting.

[BibT_eX]

[DOI]

Alexander Lochmann

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

2019

Abstract Completion, Formalized.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2019

Tools in Term Rewriting for Education.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, 2019

Confluence Competition 2019.

[BibT_eX]

[DOI]

Kiraku Shintani

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

Composing Proof Terms.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 27, 2019

2018

Completion for Logically Constrained Rewriting.

[BibT_eX]

[DOI]

Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, 2018

ProTeM: A Proof Term Manipulator (System Description).

[BibT_eX]

[DOI]

Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, 2018

Confluence Competition 2018.

[BibT_eX]

[DOI]

Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, 2018

FORT 2.0.

[BibT_eX]

[DOI]

Franziska Rapp

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

Cops and CoCoWeb: Infrastructure for Confluence Tools.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017

Preface: Selected Extended Papers of CADE 2015.

[BibT_eX]

[DOI]

Amy P. Felty

J. Autom. Reason., 2017

CoCoWeb - A Convenient Web Interface for Confluence Tools.

[BibT_eX]

[DOI]

CoRR, 2017

Complexity of Conditional Term Rewriting.

[BibT_eX]

[DOI]

Cynthia Kop

Thomas Sternagel

Log. Methods Comput. Sci., 2017

Infinite Runs in Abstract Completion.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, 2017

Constructing Cycles in the Simplex Method for DPLL(T).

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing - ICTAC 2017, 2017

CSI: New Evidence - A Progress Report.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 26, 2017

2016

Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems.

[BibT_eX]

[DOI]

Franziska Rapp

Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, 2016

Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

2015

Layer Systems for Proving Confluence.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2015

Beyond polynomials and Peano arithmetic - automation of elementary and ordinal interpretations.

[BibT_eX]

[DOI]

J. Symb. Comput., 2015

Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules.

[BibT_eX]

[DOI]

Proceedings of the 26th International Conference on Rewriting Techniques and Applications, 2015

Conditional Complexity.

[BibT_eX]

[DOI]

Cynthia Kop

Thomas Sternagel

Proceedings of the 26th International Conference on Rewriting Techniques and Applications, 2015

Leftmost Outermost Revisited.

[BibT_eX]

[DOI]

Georg Moser

Proceedings of the 26th International Conference on Rewriting Techniques and Applications, 2015

2014

Polynomial Interpretations over the Natural, Rational and Real Numbers Revisited.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2014

Conditional Confluence (System Description).

[BibT_eX]

[DOI]

Thomas Sternagel

Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

A New and Formalized Proof of Abstract Completion.

[BibT_eX]

[DOI]

Christian Sternagel

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

AC-KBO Revisited.

[BibT_eX]

[DOI]

Proceedings of the Functional and Logic Programming - 12th International Symposium, 2014

2013

Multi-Completion with Termination Tools.

[BibT_eX]

[DOI]

J. Autom. Reason., 2013

Uncurrying for Termination and Complexity.

[BibT_eX]

[DOI]

J. Autom. Reason., 2013

Beyond Peano Arithmetic - Automatically Proving Termination of the Goodstein Sequence.

[BibT_eX]

[DOI]

Proceedings of the 24th International Conference on Rewriting Techniques and Applications, 2013

Normalized Completion Revisited.

[BibT_eX]

[DOI]

Proceedings of the 24th International Conference on Rewriting Techniques and Applications, 2013

2012

Preface.

[BibT_eX]

[DOI]

Takahito Aoto

Theor. Comput. Sci., 2012

Ordinals and Knuth-Bendix Orders.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

On the Domain and Dimension Hierarchy of Matrix Interpretations.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Matrix Interpretations for Polynomial Derivational Complexity of Rewrite Systems.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

2011

Labelings for Decreasing Diagrams.

[BibT_eX]

[DOI]

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011

Revisiting Matrix Interpretations for Proving Termination of Term Rewriting.

[BibT_eX]

[DOI]

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011

Layer Systems for Proving Confluence.

[BibT_eX]

[DOI]

Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2011

Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems.

[BibT_eX]

[DOI]

Proceedings of the Algebraic Informatics - 4th International Conference, 2011

CSI - A Confluence Tool.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

AC Completion with Termination Tools.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

Uncurrying for Innermost Termination and Derivational Complexity

[BibT_eX]

[DOI]

Proceedings of the Proceedings 5th International Workshop on Higher-Order Rewriting, 2010

Finding and Certifying Loops.

[BibT_eX]

[DOI]

Proceedings of the SOFSEM 2010: Theory and Practice of Computer Science, 2010

Optimizing mkbTT.

[BibT_eX]

[DOI]

Proceedings of the 21st International Conference on Rewriting Techniques and Applications, 2010

Polynomial Interpretations over the Reals do not Subsume Polynomial Interpretations over the Integers.

[BibT_eX]

[DOI]

Proceedings of the 21st International Conference on Rewriting Techniques and Applications, 2010

Satisfiability of Non-linear (Ir)rational Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Termination Tools in Ordered Completion.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

Monotonicity Criteria for Polynomial Interpretations over the Naturals.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

Decreasing Diagrams and Relative Termination.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009

KBO Orientability.

[BibT_eX]

[DOI]

J. Autom. Reason., 2009

Constraint-Based Multi-Completion Procedures for Term Rewriting Systems.

[BibT_eX]

[DOI]

IEICE Trans. Inf. Syst., 2009

Match-bounds revisited.

[BibT_eX]

[DOI]

Inf. Comput., 2009

On the Complexity of Deciding Call-by-Need

[BibT_eX]

[DOI]

CoRR, 2009

Tyrolean Termination Tool 2.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 20th International Conference, 2009

Beyond Dependency Graphs.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2009

2008

Transforming SAT into Termination of Rewriting.

[BibT_eX]

[DOI]

Christian Sternagel

Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming, 2008

Preface.

[BibT_eX]

[DOI]

Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming, 2008

Root-Labeling.

[BibT_eX]

[DOI]

Christian Sternagel

Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008

Maximal Termination.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008

Uncurrying for Termination.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2008

Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems.

[BibT_eX]

[DOI]

Proceedings of the Language and Automata Theory and Applications, 2008

Multi-completion with Termination Tools (System Description).

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

Increasing Interpretations.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 9th International Conference, 2008

2007

Tyrolean termination tool: Techniques and features.

[BibT_eX]

[DOI]

Inf. Comput., 2007

Innermost Termination of Rewrite Systems by Labeling.

[BibT_eX]

[DOI]

Proceedings of the 7th International Workshop on Reduction Strategies in Rewriting and Programming, 2007

Constraints for Argument Filterings.

[BibT_eX]

[DOI]

Proceedings of the SOFSEM 2007: Theory and Practice of Computer Science, 2007

SAT Solving for Termination Analysis with Polynomial Interpretations.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2007

Satisfying KBO Constraints.

[BibT_eX]

[DOI]

Proceedings of the Term Rewriting and Applications, 18th International Conference, 2007

Proving Termination of Rewrite Systems Using Bounds.

[BibT_eX]

[DOI]

Proceedings of the Term Rewriting and Applications, 18th International Conference, 2007

Implementing RPO and POLO using SAT.

[BibT_eX]

[DOI]

Proceedings of the Deduction and Decision Procedures, 30.09. - 05.10.2007, 2007

Predictive Labeling with Dependency Pairs Using SAT.

[BibT_eX]

[DOI]

Adam Koprowski

Proceedings of the Automated Deduction, 2007

2006

Predictive Labeling.

[BibT_eX]

[DOI]

Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

2005

Decidable call-by-need computations in term rewriting.

[BibT_eX]

[DOI]

Inf. Comput., 2005

Tyrolean Termination Tool.

[BibT_eX]

[DOI]

Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

2004

Transformation techniques for context-sensitive rewrite systems.

[BibT_eX]

[DOI]

J. Funct. Program., 2004

Dependency Pairs Revisited.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 15th International Conference, 2004

New completeness results for lazy conditional narrowing.

[BibT_eX]

[DOI]

Mircea Marin

Proceedings of the 6th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2004

Polynomial Interpretations with Negative Coefficients.

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence and Symbolic Computation, 2004

2003

Tsukuba Termination Tool.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

Automating the Dependency Pair Method.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2002

Complete Selection Functions for a Lazy Conditional Narrowing Calculus.

[BibT_eX]

[DOI]

Taro Suzuki

Mohamed Hamada

J. Funct. Log. Program., 2002

Relative Undecidability in Term Rewriting: II. The Confluence Hierarchy.

[BibT_eX]

[DOI]

Inf. Comput., 2002

Relative Undecidability in Term Rewriting: I. The Termination Hierarchy.

[BibT_eX]

[DOI]

Inf. Comput., 2002

Approximations for Strategies and Termination.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Workshop on Reduction Strategies in Rewriting and Programming, 2002

Innermost Termination of Context-Sensitive Rewriting.

[BibT_eX]

[DOI]

Proceedings of the Developments in Language Theory, 6th International Conference, 2002

2001

On the Modularity of Deciding Call-by-Need.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2001

A Complete Selection Function for Lazy Conditional Narrowing.

[BibT_eX]

[DOI]

Taro Suzuki

Proceedings of the Functional and Logic Programming, 5th International Symposium, 2001

Approximating Dependency Graphs Using Tree Automata Techniques.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

2000

Equational Termination by Semantic Labelling.

[BibT_eX]

[DOI]

Hitoshi Ohsaki

Proceedings of the Computer Science Logic, 2000

Eliminating Dummy Elimination.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2000

1999

Transforming Context-Sensitive Rewrite Systems.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 10th International Conference, 1999

Term Rewriting.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 13th International Workshop, 1999

1998

A Deterministic Lazy Narrowing Calculus.

[BibT_eX]

[DOI]

Satoshi Okui

J. Symb. Comput., 1998

Strongly Sequential and Inductively Sequential Term Rewriting Systems.

[BibT_eX]

[DOI]

Michael Hanus

Salvador Lucas

Inf. Process. Lett., 1998

1997

Simple Termination of Rewrite Systems.

[BibT_eX]

[DOI]

Hans Zantema

Theor. Comput. Sci., 1997

Logicality of Conditional Rewrite Systems.

[BibT_eX]

[DOI]

Proceedings of the TAPSOFT'97: Theory and Practice of Software Development, 1997

Relative Undecidability in the Termination Hierarchy of Single Rewrite Rules.

[BibT_eX]

[DOI]

Proceedings of the TAPSOFT'97: Theory and Practice of Software Development, 1997

Call by Need Computations to Root-Stable Form.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of POPL'97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997

Type Introduction for Equational Rewriting.

[BibT_eX]

[DOI]

Hitoshi Ohsaki

Proceedings of the Logical Foundations of Computer Science, 4th International Symposium, 1997

Decidable Call by Need Computations in term Rewriting (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1997

1996

Relative Undecidability in Term Rewriting.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 10th International Workshop, 1996

Transforming Termination by Self-Labelling.

[BibT_eX]

[DOI]

Hitoshi Ohsaki

Hans Zantema

Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

1995

Lazy Narrowing: Strong Completeness and Eager Variable Elimination.

[BibT_eX]

Satoshi Okui

Proceedings of the 9th International Workshop on Unification, 1995

Lazy Narrowing: Strong Completeness and Eager Variable Elimination (Extended Abstract).

[BibT_eX]

[DOI]

Satoshi Okui

Proceedings of the TAPSOFT'95: Theory and Practice of Software Development, 1995

Level-Confluence of Conditional Rewrite Systems with Extra Variables in Right-Hand Sides.

[BibT_eX]

[DOI]

Taro Suzuki

Proceedings of the Rewriting Techniques and Applications, 6th International Conference, 1995

A Complete Narrowing Calculus for Higher-Order Functional Logic Programming

[BibT_eX]

[DOI]

Koichi Nakahara

Proceedings of the Programming Languages: Implementations, 1995

1994

Modularity of Confluence: A Simplified Proof.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1994

Completeness Results for Basic Narrowing.

[BibT_eX]

[DOI]

Erik Hamoen

Appl. Algebra Eng. Commun. Comput., 1994

Simple Termination Revisited.

[BibT_eX]

[DOI]

Hans Zantema

Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

A Sequential Reduction Strategy.

[BibT_eX]

[DOI]

Sergio Antoy

Proceedings of the Algebraic and Logic Programming, 4th International Conference, 1994

1993

Modular Properties of Conditional Term Rewriting Systems

[BibT_eX]

[DOI]

Inf. Comput., May, 1993

Simple Termination is Difficult.

[BibT_eX]

[DOI]

Bernhard Gramlich

Proceedings of the Rewriting Techniques and Applications, 5th International Conference, 1993

1992

Completeness of Combinations of Conditional Constructor Systems.

[BibT_eX]

[DOI]

Proceedings of the Conditional Term Rewriting Systems, Third International Workshop, 1992

Counterexamples to Completeness Results for Basic Narrowing (Extended Abstract).

[BibT_eX]

[DOI]

Erik Hamoen

Proceedings of the Algebraic and Logic Programming, 1992

1991

Sequentiality in Orthogonal Term Rewriting Systems.

[BibT_eX]

[DOI]

Jan Willem Klop

J. Symb. Comput., 1991

Completeness of Combinations of Constructor Systems.

[BibT_eX]

[DOI]

Yoshihito Toyama

Proceedings of the Rewriting Techniques and Applications, 4th International Conference, 1991

1990

Confluence of the Disjoint Union of Conditional Term Rewriting Systems.

[BibT_eX]

[DOI]

Proceedings of the Conditional and Typed Rewriting Systems, 1990

1989

Modular Aspects of Properties of Term Rewriting Systems Related to Normal Forms.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 3rd International Conference, 1989

A Sufficient Condition for the Termination of the Direct Sum of Term Rewriting Systems

[BibT_eX]

[DOI]