Orderings for term-rewriting systems
From MaRDI portal
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
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)