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
- Theorem proving with group presentations: examples and questions
- On fairness of completion-based theorem proving strategies
- On termination of the direct sum of term-rewriting systems
- A recursive path ordering for higher-order terms in η-long β-normal form
- C-expressions: A variable-free calculus for equational logic programming
- Termination tools in ordered completion
- On the recursive decomposition ordering with lexicographical status and other related orderings
- Modularity of simple termination of term rewriting systems with shared constructors
- Match-bounds revisited
- Theories of orders on the set of words
- Term rewriting induction
- Rewrite method for theorem proving in first order theory with equality
- Set of support, demodulation, paramodulation: a historical perspective
- An efficient subsumption test pipeline for BS(LRA) clauses
- A superposition oriented theorem prover
- Generalized sufficient conditions for modular termination of rewriting
- Simple termination of rewrite systems
- Parameter-preserving data type specifications
- The undecidability of self-embedding for finite semi-Thue and Thue systems
- On finite representations of infinite sequences of terms
- Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered
- A new method for undecidability proofs of first order theories
- A characterisation of multiply recursive functions with Higman's lemma.
- A fully syntactic AC-RPO.
- scientific article; zbMATH DE number 3821100 (Why is no real title available?)
- 10th Asian Logic Conference
- AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS
- Termination proofs by multiset path orderings imply primitive recursive derivation lengths
- Higher-order interpretations and program complexity
- Invariants, patterns and weights for ordering terms
- Complete equational unification based on an extension of the Knuth-Bendix completion procedure
- Path of subterms ordering and recursive decomposition ordering revisited
- Term orderings for non-reachability of (conditional) rewriting
- The Computability Path Ordering: The End of a Quest
- The order types of termination orderings on monadic terms, strings and multisets
- Normal higher-order termination
- E-unification based on generalized embedding
- On total regulators generated by derivation relations
- Implementing contextual rewriting
- Schematization of infinite sets of rewrite rules generated by divergent completion processes
- Proving termination of context-sensitive rewriting with MU-TERM
- Coq formalization of the higher-order recursive path ordering
- An effective proof of the well-foundedness of the multiset path ordering
- Enhancing dependency pair method using strong computability in simply-typed term rewriting
- Quasi-interpretations. A way to control resources
- A maximal-literal unit strategy for horn clauses
- The logic of public announcements, common knowledge, and private suspicions
- Transforming termination by self-labelling
- Minimal bad sequences are necessary for a uniform Kruskal theorem
- Termination of graph transformation systems using weighted subgraph counting
- A complete characterization of termination of 0p 1q→1r 0s
- Rewriting systems of Coxeter groups
- An improved general path order
- What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory
- On recursive path ordering
- Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
- Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
- Refutational theorem proving using term-rewriting systems
- scientific article; zbMATH DE number 7379291 (Why is no real title available?)
- Generating polynomial orderings for termination proofs
- On deciding satisfiability by theorem proving with speculative inferences
- Extensions and comparison of simplification orderings
- Polynomials over the reals in proofs of termination : from theory to practice
- Proving termination of context-sensitive rewriting by transformation
- Determinization of conditional term rewriting systems
- Building exact computation sequences
- Analysing the implicit complexity of programs.
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- Complexity analysis of term-rewriting systems
- Towards a foundation of completion procedures as semidecision procedures
- Size-based termination of higher-order rewriting
- Abstract data type systems
- Transforming SAT into termination of rewriting
- Theorem-proving with resolution and superposition
- A notation for lambda terms. A generalization of environments
- Algebra of communicating processes with abstraction
- R n - and G n -logics
- Algebra and automated deduction
- Walther recursion
- CLP(\(\mathsf{H}\)): constraint logic programming for hedges
- An universal termination condition for solving goals in equational languages
- Mechanically proving termination using polynomial interpretations
- Superposition with completely built-in abelian groups
- Finite complete rewriting systems for groups
- Combinable Extensions of Abelian Groups
- The undecidability of iterated modal relativization
- Logic and functional programming by retractions : operational semantics
- Proving termination of (conditional) rewrite systems. A semantic approach
- A calculus for and termination of rippling
- Leanest quasi-orderings
- Elimination transformations for associative-commutative rewriting systems
- Proof normalization for resolution and paramodulation
- Defining recursive predicates in graph orders
- On the longest perpetual reductions in orthogonal expression reduction systems
- SAT solving for termination proofs with recursive path orders and dependency pairs
- Termination of rewriting
- AC-KBO revisited
- Simplification orderings: Putting them to the test
- Rewriting techniques for program synthesis
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)
