Proving termination with multiset orderings

DOI10.1145/359138.359142zbMath0431.68016OpenAlexW2014030742WikidataQ56814376 ScholiaQ56814376MaRDI QIDQ3868730

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

zbMATH Keywords

production systems term rewriting systems program verification program correctness program termination reduction rules multiset ordering bags

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Termination of term rewriting by interpretation, A maximal-literal unit strategy for horn clauses, A proof system for conditional algebraic specifications, A survey of ordinal interpretations of type ɛ0 for termination of rewriting systems, Knuth-bendix completion of horn clause programs for restricted linear resolution and paramodulation, Completion procedures as semidecision procedures, SOME EXACT SEQUENCES FOR THE HOMOTOPY (BI-)MODULE OF A MONOID, Trees, ordinals and termination, Proof normalization for resolution and paramodulation, A local termination property for term rewriting systems, Rewriting techniques for program synthesis, On the correctness of a distributed memory Gröbner basis algorithm, Topics in termination, Dummy elimination in equational rewriting, Dummy elimination: Making termination easier, Mobile Processes and Termination, Reduction relations for monoid semirings, HOW MUCH PROPOSITIONAL LOGIC SUFFICES FOR ROSSER’S ESSENTIAL UNDECIDABILITY THEOREM?, On an interpretation of second order quantification in first order intuitionistic propositional logic, Size-based termination of higher-order rewriting, Implementing term rewriting by jungle evaluation, Lazy narrowing: Strong completeness and eager variable elimination (extended abstract), Reasoning about vectors: satisfiability modulo a theory of sequences, Contraction-free sequent calculi for intuitionistic logic, Complete equational unification based on an extension of the Knuth-Bendix completion procedure, Labelled Calculi for Łukasiewicz Logics, Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications, A Completion Method to Decide Reachability in Rewrite Systems, A multi-dimensional terminological knowledge representation language, Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities, Type-theoretic approaches to ordinals, Checking Admissibility Using Natural Dualities, Weighted models for higher-order computation, A Lambda-Free Higher-Order Recursive Path Order, Unnamed Item, The order types of termination orderings on monadic terms, strings and multisets, The Ideal Approach to Computing Closed Subsets in Well-Quasi-orderings, Generic top-down discrimination for sorting and partitioning in linear time, Termination of theorem proving by reuse, Canonical Ground Horn Theories, Simulating Finite Eilenberg Machines with a Reactive Engine, Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria, Tableau methods for a logic with term declarations, Unnamed Item, Unique normal form property of compatible term rewriting systems: A new proof of Chew's theorem, Combining matching algorithms: The regular case, Ensuring termination by typability, A general framework to build contextual cover set induction provers, Two applications of analytic functors, Formalizing Bachmair and Ganzinger's ordered resolution prover, A SAT-Based Approach to Size Change Termination with Global Ranking Functions, Decision Procedures for Automating Termination Proofs, Induction using term orderings, Simple termination revisited, Termination orderings for rippling, Total termination of term rewriting, Unnamed Item, A Framework for Certified Self-Stabilization, Unnamed Item, Reachability in Petri Nets with Inhibitor Arcs, Extensions of arithmetic for proving termination of computations, Uniform interpolation and the existence of sequent calculi, Termination Analysis of CHR Revisited, Random Ordering of Semiprimes, Formally verified tableau-based reasoners for a description logic, Contextual equivalence for inductive definitions with binders in higher order typed functional programming, Completeness results for basic narrowing, A semantic account of strong normalization in linear logic, A theory for nondeterminism, parallelism, communication, and concurrency, Proof theory for lattice-ordered groups, The translation power of top-down tree-to-graph transducers, 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, On proving the termination of algorithms by machine, Constructing recursion operators in intuitionistic type theory, AC simplifications and closure redundancies in the superposition calculus, On the modularity of termination of term rewriting systems, Buchberger's algorithm: The term rewriter's point of view, 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, Paramodulation with non-monotonic orderings and simplification, Total termination of term rewriting, Orderings for term-rewriting systems, Infinite complete group presentations, A geometrical approach to multiset orderings, Leanest quasi-orderings, Equational problems and disunification, Linear and unit-resulting refutations for Horn theories, An improved general path order, On unification and admissible rules in Gabbay-de Jongh logics, Normal forms for fuzzy logics: a proof-theoretic approach, Jumping and escaping: modular termination and the abstract path ordering, Simple termination of rewrite systems, A note on simplification orderings, Termination of rewrite relations on $\lambda$-terms based on Girard's notion of reducibility, Unique parallel decomposition in branching and weak bisimulation semantics, Deciding the word problem in the union of equational theories., Intermutation, Superposition decides the first-order logic fragment over ground theories, On deciding satisfiability by theorem proving with speculative inferences, Proof pearl: a formal proof of Higman's lemma in ACL2, Definability in dynamic logic, Equational completion in order-sorted algebras, A rationale for conditional equational programming, Uniform interpolation and sequent calculi in modal logic, Conditional equational theories and complete sets of transformations, On multiset orderings, Posets admitting a unique order-compatible topology, On some homotopical and homological properties of monoid presentations., Skolemization and Herbrand theorems for lattice-valued logics, 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, Lazy narrowing: strong completeness and eager variable elimination, Sequent calculi for intuitionistic Gödel-Löb logic, Towards a foundation of completion procedures as semidecision procedures, Modularity in noncopying term rewriting, Natural termination, On multiset ordering, Mathematics of multisets: a unified approach, Complete axiomatizations of some quotient term algebras, On weakly confluent monadic string-rewriting systems, Rippling: A heuristic for guiding inductive proofs, A general framework for Noetherian well ordered polynomial reductions, A general criterion for avoiding infinite unfolding during partial deduction, On the computational strength of pure ambient calculi, Deleting string rewriting systems preserve regularity, Hypergraph polytopes, Unification in a combination of arbitrary disjoint equational theories, Variadic equational matching in associative and commutative theories, The Hydra battle and Cichon's principle, A complexity tradeoff in ranking-function termination proofs, A descriptive type foundation for RDF Schema, Linearizing well quasi-orders and bounding the length of bad sequences, Conditional narrowing modulo a set of equations, Completion for rewriting modulo a congruence, Using forcing to prove completeness of resolution and paramodulation, A completion procedure for conditional equations, Superposition theorem proving for abelian groups represented as integer modules, Partial orderings for sets of multisets, Proof of termination of the rewriting system SUBSET on CCL, Decidability of behavioural equivalence in unary PCF, Giles's game and the proof theory of Łukasiewicz logic, Differential dynamic logic for hybrid systems, Context unification with one context variable, A uniform framework for term and graph rewriting applied to combined systems, Equality between functionals in the presence of coproducts, On terminating lemma speculations., Self-stabilizing extensions for message-passing systems, Set of support, demodulation, paramodulation: a historical perspective, Ground joinability and connectedness in the superposition calculus, A framework for approximate generalization in quantitative theories, The G4i analogue of a G3i sequent calculus, Modularity of confluence: A simplified proof, Termination orderings for associative-commutative rewriting systems, Confluence by decreasing diagrams, A derived algorithm for evaluating $\varepsilon$-expressions over abstract sets