REVE
From MaRDI portal
Software:40621
No author found.
Related Items (65)
On recursive path ordering ⋮ Automated deduction with associative-commutative operators ⋮ A path ordering for proving termination of AC rewrite systems ⋮ Rewriting with a nondeterministic choice operator ⋮ Buchberger's algorithm: The term rewriter's point of view ⋮ Termination of rewriting ⋮ Unification in combinations of collapse-free regular theories ⋮ Termination of string rewriting proved automatically ⋮ Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study ⋮ Simplifying conditional term rewriting systems: Unification, termination and confluence ⋮ Mechanically proving termination using polynomial interpretations ⋮ History and basic features of the critical-pair/completion procedure ⋮ Modular and incremental proofs of AC-termination ⋮ Only prime superpositions need be considered in the Knuth-Bendix completion procedure ⋮ Polynomials over the reals in proofs of termination : from theory to practice ⋮ SAT solving for termination proofs with recursive path orders and dependency pairs ⋮ Multi-completion with termination tools ⋮ Total termination of term rewriting ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Size-based termination of higher-order rewriting ⋮ AC-KBO revisited ⋮ A fully syntactic AC-RPO. ⋮ Term rewriting and beyond -- theorem proving in Isabelle ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ Equational completion in order-sorted algebras ⋮ On the recursive decomposition ordering with lexicographical status and other related orderings ⋮ A rewriting strategy to verify observational congruence ⋮ Chain properties of rule closures ⋮ Termination of term rewriting using dependency pairs ⋮ A decidable word problem without equivalent canonical term rewriting system ⋮ Combining matching algorithms: The regular case ⋮ Natural termination ⋮ A total AC-compatible ordering based on RPO ⋮ Mechanically certifying formula-based Noetherian induction reasoning ⋮ Categorical ML -- category-theoretic modular programming ⋮ Termination and completion modulo associativity, commutativity and identity ⋮ Automatic Proofs of Termination With Elementary Interpretations ⋮ Unnamed Item ⋮ Well rewrite orderings and well quasi-orderings ⋮ Unnamed Item ⋮ Unnamed Item ⋮ On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting ⋮ 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 ⋮ AC Completion with Termination Tools ⋮ Termination of rewrite systems by elementary interpretations ⋮ Conditional narrowing modulo a set of equations ⋮ Completion for rewriting modulo a congruence ⋮ Schematization of infinite sets of rewrite rules generated by divergent completion processes ⋮ Automating the Knuth Bendix ordering ⋮ Automatic Termination ⋮ Termination by completion ⋮ Proof of termination of the rewriting system SUBSET on CCL ⋮ Boolean unification - the story so far ⋮ Termination Modulo Combinations of Equational Theories ⋮ Invariants, patterns and weights for ordering terms ⋮ Unnamed Item ⋮ Refutational theorem proving using term-rewriting systems ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. I ⋮ Generating polynomial orderings ⋮ A complete superposition calculus for primal grammars ⋮ Termination orderings for associative-commutative rewriting systems ⋮ A finite Thue system with decidable word problem and without equivalent finite canonical system ⋮ Contextual rewriting as a sound and complete proof method for conditional LOG-specifications ⋮ Proving termination of (conditional) rewrite systems. A semantic approach
This page was built for software: REVE
