Termination of rewriting

From MaRDI portal
Publication:1098624

DOI10.1016/S0747-7171(87)80022-6zbMath0637.68035WikidataQ56814378 ScholiaQ56814378MaRDI QIDQ1098624

Nachum Dershowitz

Publication date: 1987

Published in: Journal of Symbolic Computation (Search for Journal in Brave)




Related Items (only showing first 100 items - show all)

Generalized sufficient conditions for modular termination of rewritingRewriting modulo isotopies in pivotal linear \((2,2)\)-categoriesOn termination of confluent one-rule string-rewriting systemsThe translation power of top-down tree-to-graph transducersSome results on the confluence property of combined term rewriting systemsAn overview of the Tecton proof systemSimple termination is difficultOn the termination of clause graph resolutionThe data type variety of stack algebrasA path ordering for proving termination of AC rewrite systemsWeights for total division orderings on stringsHead boundedness of nonterminating rewritingsEnsuring the quasi-termination of needed narrowing computationsBuchberger's algorithm: The term rewriter's point of viewProving Ramsey's theory by the cover set induction: A case and comparision study.Termination proofs for string rewriting systems via inverse match-boundsExtension functions for multiset orderingsProving termination of context-sensitive rewriting by transformationOn termination of the direct sum of term-rewriting systemsDecision procedures for the security of protocols with probabilistic encryption against offline dictionary attacksTotal termination of term rewritingNew uses of linear arithmetic in automated theorem proving by inductionA calculus for and termination of ripplingLeanest quasi-orderingsUnification in sort theories and its applicationsMechanizing and improving dependency pairsLinear and unit-resulting refutations for Horn theoriesCombination of constraint solvers for free and quasi-free structuresReasoning with conditional axiomsAn improved general path orderJumping and escaping: modular termination and the abstract path orderingInteraction nets and term-rewriting systemsSimple termination of rewrite systemsThe first-order theory of lexicographic path orderings is undecidableUnification of infinite sets of terms schematized by primal grammarsPractical algorithms for deciding path ordering constraint satisfaction.Analysing the implicit complexity of programs.Constraint-based correctness proofs for logic program transformationsModular term rewriting systems and the terminationThe derivational complexity of string rewriting systemsEquational completion in order-sorted algebrasOn the recursive decomposition ordering with lexicographical status and other related orderingsAutomated proofs of the Moufang identities in alternative ringsWeighted graphs: A tool for studying the halting problem and time complexity in term rewriting systems and logic programmingChain properties of rule closuresA note on division orderings on stringsRigid E-unification: NP-completeness and applications to equational matingsOverlap closures do not suffice for termination of general term rewriting systemsBinary decision diagrams for first-order predicate logic.Termination of just/fair computations in term rewritingRewriting modulo isotopies in Khovanov-Lauda-Rouquier's categorification of quantum groupsEfficient solution of a class of quantified constraints with quantifier prefix exists-forallWhat's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theoryTermination of term rewriting using dependency pairsSome experiments with a completion theorem proverUsing induction and rewriting to verify and complete parameterized specificationsModular termination of \(r\)-consistent and left-linear term rewriting systemsTowards a foundation of completion procedures as semidecision proceduresLoop detection in term rewriting using the eliminating unfoldingsNatural terminationA total AC-compatible ordering based on RPOSome undecidable termination problems for semi-Thue systemsA combinatory logic approach to higher-order E-unificationAssociative-commutative reduction orderingsOn the complexity of recursive path orderingsSimulation of Turing machines by a regular rewrite ruleTermination and completion modulo associativity, commutativity and identityTermination proofs by multiset path orderings imply primitive recursive derivation lengthsA field guide to equational logicA general criterion for avoiding infinite unfolding during partial deductionAdding algebraic rewriting to the untyped lambda calculusMatch-bounded string rewriting systemsRationality of division orderingsWell rewrite orderings and well quasi-orderingsA new method for undecidability proofs of first order theoriesDecision problems for semi-Thue systems with a few rulesTermination of narrowing via termination of rewritingZero, successor and equality in BDDsTotally correct logic program transformations via well-founded annotationsComplete sets of transformations for general E-unificationAutomating the Knuth Bendix orderingTermination by completionUsing forcing to prove completeness of resolution and paramodulationTheorem-proving with resolution and superpositionA completion procedure for conditional equationsRewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path orderingOn equational theories, unification, and (un)decidabilityDecidability and complexity analysis by basic paramodulationTermination of narrowing revisitedPattern-matching algorithms based on term rewrite systemsPartial completion of equational theoriesOn terminating lemma speculations.Context-sensitive rewriting strategiesSet of support, demodulation, paramodulation: a historical perspectiveSimplification orderings: Putting them to the testModular termination proofs for rewriting using dependency pairsGenerating polynomial orderingsAutomated proofs of equality problems in Overbeek's competitionDeductive and inductive synthesis of equational programsProving termination of (conditional) rewrite systems. A semantic approach


Uses Software


Cites Work


This page was built for publication: Termination of rewriting