Proving termination with multiset orderings
From MaRDI portal
Publication:3868730
DOI10.1145/359138.359142zbMath0431.68016WikidataQ56814376 ScholiaQ56814376MaRDI QIDQ3868730
Nachum Dershowitz, Zohar Manna
Publication date: 1979
Published in: Communications of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/359138.359142
production systems; term rewriting systems; program verification; program correctness; program termination; reduction rules; multiset ordering; bags
68W30: Symbolic computation and algebraic computation
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
The order types of termination orderings on monadic terms, strings and multisets, Extensions of arithmetic for proving termination of computations, SOME EXACT SEQUENCES FOR THE HOMOTOPY (BI-)MODULE OF A MONOID, A multi-dimensional terminological knowledge representation language, A SAT-Based Approach to Size Change Termination with Global Ranking Functions, Termination Analysis of CHR Revisited, Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria, Tableau methods for a logic with term declarations, Unique normal form property of compatible term rewriting systems: A new proof of Chew's theorem, A general framework to build contextual cover set induction provers, Two applications of analytic functors, Unification in a combination of arbitrary disjoint equational theories, Orderings for term-rewriting systems, Lazy narrowing: strong completeness and eager variable elimination, Towards a foundation of completion procedures as semidecision procedures, Modularity in noncopying term rewriting, Natural termination, Complete axiomatizations of some quotient term algebras, On weakly confluent monadic string-rewriting systems, Rippling: A heuristic for guiding inductive proofs, Deleting string rewriting systems preserve regularity, Using forcing to prove completeness of resolution and paramodulation, A completion procedure for conditional equations, Leanest quasi-orderings, Normal forms for fuzzy logics: a proof-theoretic approach, Equational completion in order-sorted algebras, A rationale for conditional equational programming, Conditional equational theories and complete sets of transformations, On some homotopical and homological properties of monoid presentations., A complexity tradeoff in ranking-function termination proofs, Termination orderings for associative-commutative rewriting systems, A theory for nondeterminism, parallelism, communication, and concurrency, Constructing recursion operators in intuitionistic type theory, Termination of rewriting, Path of subterms ordering and recursive decomposition ordering revisited, The Church-Rosser property for ground term-rewriting systems is decidable, History and basic features of the critical-pair/completion procedure, Extension functions for multiset orderings, Only prime superpositions need be considered in the Knuth-Bendix completion procedure, Critical pair criteria for completion, On termination of the direct sum of term-rewriting systems, A geometrical approach to multiset orderings, Equational problems and disunification, A note on simplification orderings, Definability in dynamic logic, On multiset orderings, Posets admitting a unique order-compatible topology, What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory, Combining matching algorithms: The regular case, A general criterion for avoiding infinite unfolding during partial deduction, Conditional narrowing modulo a set of equations, Completion for rewriting modulo a congruence, Superposition theorem proving for abelian groups represented as integer modules, Decidability of behavioural equivalence in unary PCF, Self-stabilizing extensions for message-passing systems, Modularity of confluence: A simplified proof, Confluence by decreasing diagrams, A derived algorithm for evaluating \(\varepsilon\)-expressions over abstract sets, Completeness results for basic narrowing, The translation power of top-down tree-to-graph transducers, On proving the termination of algorithms by machine, On the modularity of termination of term rewriting systems, Buchberger's algorithm: The term rewriter's point of view, Simple termination of rewrite systems, Deciding the word problem in the union of equational theories., A uniform framework for term and graph rewriting applied to combined systems, On the computational strength of pure ambient calculi, Partial orderings for sets of multisets, Proof of termination of the rewriting system SUBSET on CCL, Equality between functionals in the presence of coproducts, On terminating lemma speculations., Right-linear half-monadic term rewrite systems, Three-variable statements of set-pairing, Deciding confluence of certain term rewriting systems in polynomial time, Intersection types for explicit substitutions, A linear time algorithm for monadic querying of indefinite data over linearly ordered domains, Decidability of bounded second order unification, Total termination of term rewriting, Infinite complete group presentations, Linear and unit-resulting refutations for Horn theories, An improved general path order, Ensuring termination by typability, Reduction relations for monoid semirings, Implementing term rewriting by jungle evaluation, Labelled Calculi for Łukasiewicz Logics, Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities, Unnamed Item, On an interpretation of second order quantification in first order intuitionistic propositional logic, Contraction-free sequent calculi for intuitionistic logic
