Orderings for term-rewriting systems

Cites work

scientific article; zbMATH DE number 3635501 (Why is no real title available?)
scientific article; zbMATH DE number 3299786 (Why is no real title available?)
scientific article; zbMATH DE number 3198033 (Why is no real title available?)
scientific article; zbMATH DE number 3068536 (Why is no real title available?)
A note on simplification orderings
Algebraic simplification
Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
Automatic Proofs of Theorems in Analysis Using Nonstandard Techniques
Complete Sets of Reductions for Some Equational Theories
Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
Decision procedures for real and p‐adic fields
New decision algorithms for finitely presented commutative semigroups
Proving termination with multiset orderings
Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture

Cited in

(only showing first 100 items - show all)

Using forcing to prove completeness of resolution and paramodulation
A new method for undecidability proofs of first order theories
A geometrical approach to multiset orderings
Analysing the implicit complexity of programs.
Refutational theorem proving using term-rewriting systems
A calculus for and termination of rippling
Regaining cut admissibility in deduction modulo using abstract completion
Superposition with completely built-in abelian groups
Using unavoidable set of trees to generalize Kruskal's theorem
Proving termination of context-sensitive rewriting with MU-TERM
Termination proofs by multiset path orderings imply primitive recursive derivation lengths
The undecidability of iterated modal relativization
Finite complete rewriting systems for the Jantzen monoid and the Greendlinger group
On the recursive decomposition ordering with lexicographical status and other related orderings
Theories of orders on the set of words
Higher-order interpretations and program complexity
Mechanically proving termination using polynomial interpretations
Building exact computation sequences
Modularity of simple termination of term rewriting systems with shared constructors
Transforming termination by self-labelling
Type-based homeomorphic embedding for online termination
Parameter-preserving data type specifications
Quasi-interpretations. A way to control resources
The undecidability of self-embedding for finite semi-Thue and Thue systems
Proof of termination of the rewriting system SUBSET on CCL
Outermost ground termination
Match-bounds revisited
Termination orderings for associative-commutative rewriting systems
Incremental termination proofs and the length of derivations
Topics in termination
Complete equational unification based on an extension of the Knuth-Bendix completion procedure
Term rewriting: Some experimental results
Automating the Knuth Bendix ordering
On deciding satisfiability by theorem proving with speculative inferences
The logic of public announcements, common knowledge, and private suspicions
Path of subterms ordering and recursive decomposition ordering revisited
Termination by completion
Schematization of infinite sets of rewrite rules generated by divergent completion processes
Conditional rewriting in focus
Natural termination
Reductions in tree replacement systems
Proving semantical equivalence of data specifications
Two applications of analytic functors
Sufficient conditions for modular termination of conditional term rewriting systems
An overview of LP, the Larch Prover
Paramodulation with non-monotonic orderings and simplification
Theorem-proving with resolution and superposition
Termination of term rewriting using dependency pairs
Enhancing dependency pair method using strong computability in simply-typed term rewriting
Extensions and comparison of simplification orderings
Finite complete rewriting systems for groups
On termination of the direct sum of term-rewriting systems
Weights for total division orderings on strings
C-expressions: A variable-free calculus for equational logic programming
A maximal-literal unit strategy for horn clauses
Polynomials over the reals in proofs of termination : from theory to practice
Correspondences between classical, intuitionistic and uniform provability
Algebra of communicating processes with abstraction
An improved general path order
Term rewriting induction
Proof normalization for resolution and paramodulation
Determinization of conditional term rewriting systems
Termination proofs by multiset path orderings imply primitive recursive derivation lengths
Rewriting systems of Coxeter groups
Rewrite method for theorem proving in first order theory with equality
The undecidability of self-embedding for term rewriting systems
Complexity analysis of term-rewriting systems
Deciding confluence of certain term rewriting systems in polynomial time
Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
On finite representations of infinite sequences of terms
On multiset ordering
A general framework to build contextual cover set induction provers
Mechanically certifying formula-based Noetherian induction reasoning
Termination of rewriting
Towards a foundation of completion procedures as semidecision procedures
On total regulators generated by derivation relations
A complete characterization of termination of 0p 1q→1r 0s
CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
Termination tools in ordered completion
Generalized sufficient conditions for modular termination of rewriting
On recursive path ordering
Trees, ordinals and termination
A superposition oriented theorem prover
Dummy elimination: Making termination easier
Generating polynomial orderings for termination proofs
Implementing contextual rewriting
What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory
A characterisation of multiply recursive functions with Higman's lemma.
A fully syntactic AC-RPO.
Abstract data type systems
Term orderings for non-reachability of (conditional) rewriting
AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS
Equational completion in order-sorted algebras
Leanest quasi-orderings
scientific article; zbMATH DE number 3860380 (Why is no real title available?)
Elimination transformations for associative-commutative rewriting systems
scientific article; zbMATH DE number 3926235 (Why is no real title available?)
Embedding with patterns and associated recursive path ordering
Corrigendum to ``Termination of rewriting
A termination ordering for higher order rewrite systems

Describes a project that uses

Uses Software

REDUCE
NQTHM

This page was built for publication: Orderings for term-rewriting systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q593789)