REVE

swMATH28907MaRDI QIDQ40621FDOQ40621

Author name not available (Why is that?)

Described by source

• Termination of rewriting systems by polynomial interpretations and its implementation

Cited In (65)

• Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study
• On the recursive decomposition ordering with lexicographical status and other related orderings
• A rewriting strategy to verify observational congruence
• Categorical ML -- category-theoretic modular programming
• Total termination of term rewriting
• A decidable word problem without equivalent canonical term rewriting system
• Rewriting with a nondeterministic choice operator
• A fully syntactic AC-RPO.
• Chain properties of rule closures
• Completion for rewriting modulo a congruence
• Invariants, patterns and weights for ordering terms
• Term rewriting and beyond -- theorem proving in Isabelle
• Conditional narrowing modulo a set of equations
• Schematization of infinite sets of rewrite rules generated by divergent completion processes
• On recursive path ordering
• Refutational theorem proving using term-rewriting systems
• Buchberger's algorithm: The term rewriter's point of view
• Polynomials over the reals in proofs of termination : from theory to practice
• Proving termination by dependency pairs and inductive theorem proving
• Simplifying conditional term rewriting systems: Unification, termination and confluence
• Size-based termination of higher-order rewriting
• Mechanically proving termination using polynomial interpretations
• Proving termination of (conditional) rewrite systems. A semantic approach
• Unification in combinations of collapse-free regular theories
• Termination of rewriting
• Combining matching algorithms: The regular case
• Termination orderings for associative-commutative rewriting systems
• Termination of term rewriting using dependency pairs
• Termination and completion modulo associativity, commutativity and identity
• Title not available (Why is that?)
• Generating polynomial orderings
• Automating the Knuth Bendix ordering
• Termination by completion
• Contextual rewriting as a sound and complete proof method for conditional LOG-specifications
• Well rewrite orderings and well quasi-orderings
• Automatic Proofs of Termination With Elementary Interpretations
• A finite Thue system with decidable word problem and without equivalent finite canonical system
• Boolean unification - the story so far
• AC Completion with Termination Tools
• Title not available (Why is that?)
• Termination Modulo Combinations of Equational Theories
• Equational completion in order-sorted algebras
• Multi-completion with termination tools
• Automated deduction with associative-commutative operators
• Outermost ground termination
• History and basic features of the critical-pair/completion procedure
• Proof of termination of the rewriting system SUBSET on CCL
• Preuves de terminaison de systèmes de réécriture fondées sur les interprétations polynomiales. Une méthode basée sur le théorème de Sturm
• Title not available (Why is that?)
• Modular and incremental proofs of AC-termination
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Mechanically certifying formula-based Noetherian induction reasoning
• Title not available (Why is that?)
• Title not available (Why is that?)
• Termination of rewrite systems by elementary interpretations
• Termination of string rewriting proved automatically
• A total AC-compatible ordering based on RPO
• Natural termination
• Cancellative Abelian monoids and related structures in refutational theorem proving. I
• Automatic Termination
• A path ordering for proving termination of AC rewrite systems
• On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting
• A complete superposition calculus for primal grammars
• SAT solving for termination proofs with recursive path orders and dependency pairs
• AC-KBO revisited

This page was built for software: REVE