Problems in rewriting III
From MaRDI portal
Publication:5055847
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
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)
Uses Software
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)