scientific article; zbMATH DE number 1142316
From MaRDI portal
Publication:4385532
zbMath0900.68283MaRDI QIDQ4385532
Nachum Dershowitz, Jean-Pierre Jouannaud
Publication date: 14 May 1998
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (only showing first 100 items - show all)
Context rewriting ⋮ Consistency and semantics of equational definitions over predefined algebras ⋮ Collapsed tree rewriting: Completeness, confluence, and modularity ⋮ Revisiting Semantics of Interactions for Trace Validity Analysis ⋮ Associative-commutative discrimination nets ⋮ About the theory of tree embedding ⋮ Term rewriting in CTΣ ⋮ On μ-symmetric polynomials ⋮ Time bounded rewrite systems and termination proofs by generalized embedding ⋮ Narrowing directed by a graph of terms ⋮ Decidability of confluence and termination of monadic term rewriting systems ⋮ On fairness of completion-based theorem proving strategies ⋮ Proving equational and inductive theorems by completion and embedding techniques ⋮ On proving properties of completion strategies ⋮ Open problems in rewriting ⋮ Bi-rewriting, a term rewriting technique for monotonic order relations ⋮ Distributing equational theorem proving ⋮ Improving transformation systems for general E-unification ⋮ Some lambda calculi with categorical sums and products ⋮ Optimal normalization in orthogonal term rewriting systems ⋮ More problems in rewriting ⋮ Automatic termination proofs with transformation orderings ⋮ On narrowing, refutation proofs and constraints ⋮ Concurrent garbage collection for concurrent rewriting ⋮ Lazy rewriting and eager machinery ⋮ Level-confluence of conditional rewrite systems with extra variables in right-hand sides ⋮ Relating two categorical models of term rewriting ⋮ (Head-)normalization of typeable rewrite systems ⋮ Explicit substitutions with de bruijn's levels ⋮ Some independence results for equational unification ⋮ Generating polynomial orderings for termination proofs ⋮ Problems in rewriting III ⋮ Fine-grained concurrent completion ⋮ Termination of constructor systems ⋮ Dummy elimination in equational rewriting ⋮ On proving termination by innermost termination ⋮ A recursive path ordering for higher-order terms in η-long β-normal form ⋮ Modularity of termination in term graph rewriting ⋮ Confluence of terminating conditional rewrite systems revisited ⋮ The first-order theory of one-step rewriting is undecidable ⋮ On the termination problem for one-rule semi-Thue system ⋮ Decidable approximations of term rewriting systems ⋮ Semantics and strong sequentially of priority term rewriting systems ⋮ Higher-order families ⋮ Rewriting regular inequalities ⋮ Dummy elimination: Making termination easier ⋮ Unique normal forms for nonlinear term rewriting systems: Root overlaps ⋮ String Diagram Rewrite Theory I: Rewriting with Frobenius Structure ⋮ Buchberger's algorithm: The term rewriter's point of view ⋮ Equation solving in conditional AC-theories ⋮ An abstract concurrent machine for rewriting ⋮ Jungle rewriting: An abstract description of a lazy narrowing machine ⋮ A confluent relational calculus for higher-order programming with constraints ⋮ “Syntactic” AC-unification ⋮ On modularity in term rewriting and narrowing ⋮ Higher order conditional rewriting and narrowing ⋮ Buchberger's algorithm: A constraint-based completion procedure ⋮ An introduction to category-based equational logic ⋮ CPO models for infinite term rewriting ⋮ Semi-completeness of hierarchical and super-hierarchical combinations of term rewriting systems ⋮ Lazy narrowing: Strong completeness and eager variable elimination (extended abstract) ⋮ Negation elimination in equational formulae ⋮ One-rule trace-rewriting systems and confluence ⋮ Rational rewriting ⋮ Critical pairs in term graph rewriting ⋮ Well-founded coalgebras, revisited ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Proving convergence of self-stabilizing systems using first-order rewriting and regular languages ⋮ Confluence: The Unifying, Expressive Power of Locality ⋮ Functional Logic Programming: From Theory to Curry ⋮ FLIC: Application to Caching of a Dynamic Dependency Analysis for a 3D Oriented CRS ⋮ A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting ⋮ Closure of Tree Automata Languages under Innermost Rewriting ⋮ AC complement problems: Satisfiability and negation elimination ⋮ Variant Narrowing and Equational Unification ⋮ A polynomial algorithm testing partial confluence of basic semi-Thue systems ⋮ Superposition theorem proving for abelian groups represented as integer modules ⋮ Simple termination is difficult ⋮ Any ground associative-commutative theory has a finite canonical system ⋮ On Transfinite Knuth-Bendix Orders ⋮ Completion of rewrite systems with membership constraints ⋮ Completion for multiple reduction orderings ⋮ Induction using term orderings ⋮ On notions of inductive validity for first-order equational clauses ⋮ Simple termination revisited ⋮ Termination orderings for rippling ⋮ Associative-commutative deduction with constraints ⋮ AC-superposition with constraints: No AC-unifiers needed ⋮ On pot, pans and pudding or how to discover generalised critical Pairs ⋮ Total termination of term rewriting ⋮ Completeness of combinations of constructor systems ⋮ Termination proofs by multiset path orderings imply primitive recursive derivation lengths ⋮ How to win a game with features ⋮ Decidable call by need computations in term rewriting (extended abstract) ⋮ A Set-theoretic Approach to Reasoning Services for the Description Logic 𝒟 ℒ D 4,× ⋮ ON THE INVARIANCE OF GÖDEL’S SECOND THEOREM WITH REGARD TO NUMBERINGS ⋮ Type-Based Homeomorphic Embedding and Its Applications to Online Partial Evaluation ⋮ Towards an Efficient Implementation of Tree Automata Completion ⋮ Termination by absence of infinite chains of dependency pairs
This page was built for publication:
