Problems in rewriting III

DOI10.1007/3-540-59200-8_82zbMATH Open1504.68089OpenAlexW1519212137MaRDI QIDQ5055847FDOQ5055847

Authors: Nachum Dershowitz, Jean-Pierre Jouannaud, Jan Willem Klop 

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-59200-8_82

Recommendations

• More problems in rewriting
• Term Rewriting and Applications
• Rewriting
• Term Rewriting and All That
• scientific article

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cites Work

• Termination of term rewriting: Interpretation and type elimination
• Title not available (Why is that?)
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A rationale for conditional equational programming
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• A logic programming language with lambda-abstraction, function variables, and simple unification
• Title not available (Why is that?)
• Accessible Independence Results for Peano Arithmetic
• On sufficient-completeness and related properties of term rewriting systems
• Title not available (Why is that?)
• Explicit substitutions with de bruijn's levels
• Unification problems with one-sided distributivity
• Confluence by decreasing diagrams
• Title not available (Why is that?)
• Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems
• Conditional rewriting in focus
• Title not available (Why is that?)
• Automatic proofs by induction in theories without constructors
• Encompassment properties and automata with constraints
• Simple termination is difficult
• Total termination of term rewriting is undecidable
• Rewrite systems for varieties of semigroups
• Title not available (Why is that?)
• Decidability of systems of set constraints with negative constraints
• Title not available (Why is that?)
• A superposition oriented theorem prover
• A new method for undecidability proofs of first order theories
• Bounding derivation lengths with functions from the slow growing hierarchy
• COMBINING TERM REWRITING AND TYPE ASSIGNMENT SYSTEMS
• Title not available (Why is that?)
• Title not available (Why is that?)
• Modularity of strong normalization in the algebraic-λ-cube
• Title not available (Why is that?)
• Modular aspects of properties of term rewriting systems related to normal forms
• Complete axiomatizations of some quotient term algebras
• Title not available (Why is that?)
• Title not available (Why is that?)
• Clausal rewriting
• Title not available (Why is that?)
• Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
• The Church-Rosser property for ground term-rewriting systems is decidable
• Simulation of Turing machines by a regular rewrite rule
• Title not available (Why is that?)
• Confluence of the lambda calculus with left-linear algebraic rewriting
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Open problems in rewriting
• More problems in rewriting
• The first-order theory of lexicographic path orderings is undecidable
• Introduction to generalized type systems
• Title not available (Why is that?)
• LFCS '94, Logical foundations of computer science. 3rd International Symposium, St. Petersburg, Russia, July 11-14, 1994. Proceedings
• Reduction techniques for first-order reasoning
• On termination of one rule rewrite systems
• Title not available (Why is that?)
• Total termination of term rewriting
• Modularity of termination and confluence in combinations of rewrite systems with \(\lambda_\omega\)
• About the theory of tree embedding
• Set constraints with projections
• Combination techniques and decision problems for disunification
• An efficient representation of arithmetic for term rewriting
• Rewrite systems for integer arithmetic
• A partial solution for \(D\)-unification based on a reduction to AC1-unification
• Title not available (Why is that?)
• AC complement problems: Satisfiability and negation elimination
• Modular AC unification of higher-order patterns
• “Syntactic” AC-unification

Cited In (6)

• Unique normal form property of compatible term rewriting systems: A new proof of Chew's theorem
• The first-order theory of linear one-step rewriting is undecidable
• More problems in rewriting
• Thue trees
• Title not available (Why is that?)
• The first-order theory of one-step rewriting is undecidable

Uses Software

• Automath

This page was built for publication: Problems in rewriting III

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5055847)