Open problems in rewriting
From MaRDI portal
Publication:5055780
DOI10.1007/3-540-53904-2_120zbMath1503.68100OpenAlexW1550542381MaRDI QIDQ5055780
Jan Willem Klop, Nachum Dershowitz, Jean-Pierre Jouannaud
Publication date: 9 December 2022
Published in: Rewriting Techniques and Applications (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-53904-2_120
Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (9)
More problems in rewriting ⋮ Problems in rewriting III ⋮ Bubbles in modularity ⋮ The first-order theory of lexicographic path orderings is undecidable ⋮ First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification ⋮ Logicality of conditional rewrite systems ⋮ Decidability of regularity and related properties of ground normal form languages ⋮ Simple termination is difficult ⋮ Unnamed Item
Uses Software
Cites Work
- Termination of rewriting systems by polynomial interpretations and its implementation
- Term rewriting: Some experimental results
- Reduction graphs in the lambda calculus
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Refutational theorem proving using term-rewriting systems
- A rationale for conditional equational programming
- Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems
- Rewriting techniques and applications. (First International Conference), Dijon, France, May 20-22, 1985
- On sufficient-completeness and related properties of term rewriting systems
- On recursive path ordering
- n-level rewriting systems
- Rewriting techniques and applications. Bordeaux, France, May 25--27, 1987. Proceedings. (2nd International Conference)
- A refinement of strong sequentiality for term rewriting with constructors
- Systems of reductions
- Corrigendum to ``Termination of rewriting
- Associative-commutative unification
- The Church-Rosser property for ground term-rewriting systems is decidable
- Explicit representation of terms defined by counter examples
- Conditional rewrite rules: Confluence and termination
- Unique normal forms for lambda calculus with surjective pairing
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- Rewrite, rewrite, rewrite, rewrite, rewrite, \dots
- Rewriting techniques and applications. 3rd international conference, RTA-89, Chapel Hill, NC, USA, April 3--5, 1989. Proceedings
- Termination and completion modulo associativity, commutativity and identity
- Sequential evaluation strategies for parallel-or and related reduction systems
- Calcul de longueurs de chaînes de réécriture dans le monoïde libre
- Semantic confluence tests and completion methods
- Existence, Uniqueness, and Construction of Rewrite Systems
- Completion of a Set of Rules Modulo a Set of Equations
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Complete Sets of Reductions for Some Equational Theories
- Accessible Independence Results for Peano Arithmetic
- Minimal and Optimal Computations of Recursive Programs
- Introduction to generalized type systems
- Complete sets of reductions modulo associativity, commutativity and identity
- Simulation of Turing machines by a left-linear rewrite rule
- Modular aspects of properties of term rewriting systems related to normal forms
- Transfinite reductions in orthogonal term rewriting systems
- On relationship between term rewriting systems and regular tree languages
- Conditional rewriting in focus
- Extended term rewriting systems
- Clausal rewriting
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Open problems in rewriting
