scientific article
From MaRDI portal
Publication:2783416
zbMath0999.68095MaRDI QIDQ2783416
Publication date: 16 April 2002
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Research exposition (monographs, survey articles) pertaining to computer science (68-02) Grammars and rewriting systems (68Q42)
Related Items (90)
Relative termination via dependency pairs ⋮ Unnamed Item ⋮ Automatically Proving and Disproving Feasibility Conditions ⋮ mu-term: Verify Termination Properties Automatically (System Description) ⋮ The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors ⋮ Transforming orthogonal inductive definition sets into confluent term rewrite systems ⋮ A Finite Representation of the Narrowing Space ⋮ Confluence Competition 2015 ⋮ Reducing Relative Termination to Dependency Pair Problems ⋮ Algebraic simulations ⋮ Transformations of Conditional Rewrite Systems Revisited ⋮ Rota's classification problem, rewriting systems and Gröbner-Shirshov bases ⋮ Modular and incremental proofs of AC-termination ⋮ Proving termination of context-sensitive rewriting by transformation ⋮ Polynomials over the reals in proofs of termination : from theory to practice ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ Dependency pairs for proving termination properties of conditional term rewriting systems ⋮ On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs ⋮ Averaging algebras, rewriting systems and Gröbner–Shirshov bases ⋮ Elimination transformations for associative-commutative rewriting systems ⋮ Mechanizing and improving dependency pairs ⋮ Rewriting systems over similarity and generalized pseudometric spaces and their properties ⋮ Layer Systems for Proving Confluence ⋮ Modularity in term rewriting revisited ⋮ Determinization of conditional term rewriting systems ⋮ Semi-inversion of Conditional Constructor Term Rewriting Systems ⋮ Twenty years of rewriting logic ⋮ On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories ⋮ Initial Conflicts for Transformation Rules with Nested Application Conditions ⋮ Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting ⋮ Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting ⋮ Local confluence of conditional and generalized term rewriting systems ⋮ Formalizing Soundness and Completeness of Unravelings ⋮ Decreasing diagrams and relative termination ⋮ Modular Termination of Basic Narrowing ⋮ Usable Rules for Context-Sensitive Rewrite Systems ⋮ Confluence by Decreasing Diagrams ⋮ Conversion to tail recursion in term rewriting ⋮ Inverse Unfold Problem and Its Heuristic Solving ⋮ On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings ⋮ Notes on Structure-Preserving Transformations of Conditional Term Rewrite Systems ⋮ Unnamed Item ⋮ Termination of just/fair computations in term rewriting ⋮ MTT: The Maude Termination Tool (System Description) ⋮ Modularity of Confluence ⋮ Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems ⋮ The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques ⋮ Modeling dynamic programming problems over sequences and trees with inverse coupled rewrite systems ⋮ Determinization of inverted grammar programs via context-free expressions ⋮ Confluence theory for graphs ⋮ Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications ⋮ Strict coherence of conditional rewriting modulo axioms ⋮ Use of logical models for proving infeasibility in term rewriting ⋮ Free operated monoids and rewriting systems ⋮ Completion after Program Inversion of Injective Functions ⋮ Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures ⋮ Decidable call-by-need computations in term rewriting ⋮ Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications ⋮ Operational Termination of Membership Equational Programs: the Order-Sorted Way ⋮ Characterizing and proving operational termination of deterministic conditional term rewriting systems ⋮ On modularity in infinitary term rewriting ⋮ Proving operational termination of membership equational programs ⋮ On the confluence of lambda-calculus with conditional rewriting ⋮ A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems ⋮ Context-sensitive dependency pairs ⋮ On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs ⋮ Normal forms and normal theories in conditional rewriting ⋮ Proving semantic properties as first-order satisfiability ⋮ Applications and extensions of context-sensitive rewriting ⋮ Methods for Proving Termination of Rewriting-based Programming Languages by Transformation ⋮ Transformation rules with nested application conditions: critical pairs, initial conflicts \& minimality ⋮ Using well-founded relations for proving operational termination ⋮ Automatic generation of logical models with AGES ⋮ Confluence by critical pair analysis revisited ⋮ Proving Confluence of Term Rewriting Systems Automatically ⋮ Local Termination ⋮ From Outermost to Context-Sensitive Rewriting ⋮ A Fully Abstract Semantics for Constructor Systems ⋮ Modular termination of prefix-constrained term rewrite systems ⋮ Derivational complexity and context-sensitive Rewriting ⋮ Termination of narrowing revisited ⋮ Conditions for confluence of innermost terminating term rewriting systems ⋮ Termination Modulo Combinations of Equational Theories ⋮ Operational termination of conditional term rewriting systems ⋮ On-demand strategy annotations revisited: an improved on-demand evaluation strategy ⋮ Term orderings for non-reachability of (conditional) rewriting ⋮ Transformation for Refining Unraveled Conditional Term Rewriting Systems ⋮ Improving the Context-sensitive Dependency Graph ⋮ Proving Termination of Context-Sensitive Rewriting with MU-TERM ⋮ Confluence and commutation for nominal rewriting systems with atom-variables
This page was built for publication:
