The following pages link to Term Rewriting and All That (Q4702972):
Displayed 50 items.
- Effective codescent morphisms in the varieties determined by convergent term rewriting systems. (Q278228) (← links)
- Algorithms for Kleene algebra with converse (Q299194) (← links)
- Decision problems for word-hyperbolic semigroups (Q306545) (← links)
- Uncurrying for termination and complexity (Q352959) (← links)
- Paramodulation with non-monotonic orderings and simplification (Q352977) (← links)
- On unification and admissible rules in Gabbay-de Jongh logics (Q386639) (← links)
- Simulation relations for pattern matching in directed graphs (Q388784) (← links)
- Unifying sets and programs via dependent types (Q408534) (← links)
- Unification modulo homomorphic encryption (Q437037) (← links)
- A combined superposition and model evolution calculus (Q438531) (← links)
- Proving termination by dependency pairs and inductive theorem proving (Q438537) (← links)
- Proof pearl: a formal proof of Higman's lemma in ACL2 (Q438550) (← links)
- \(E\)-unification with constants vs. general \(E\)-unification (Q438584) (← links)
- Higher-dimensional normalisation strategies for acyclicity (Q456807) (← links)
- Relative locations of subwords in free operated semigroups and Motzkin words. (Q493381) (← links)
- A coherence theorem for pseudonatural transformations (Q502628) (← links)
- Satisfiability of general intruder constraints with and without a set constructor (Q507349) (← links)
- On proving confluence modulo equivalence for Constraint Handling Rules (Q511019) (← links)
- Abstract conjunctive partial deduction for the analysis and compilation of coroutines (Q511025) (← links)
- Model-theoretic methods in combined constraint satisfiability (Q556677) (← links)
- On the complexity of deduction modulo leaf permutative equations (Q556681) (← links)
- Reachability analysis over term rewriting systems (Q556686) (← links)
- A formalization of the Knuth-Bendix(-Huet) critical pair theorem (Q616850) (← links)
- Categorification, term rewriting and the Knuth-Bendix procedure (Q626714) (← links)
- Best unifiers in transitive modal logics (Q647403) (← links)
- Linearity and iterator types for Gödel's system \(\mathcal T\) (Q656851) (← links)
- The Hydra battle and Cichon's principle (Q734036) (← links)
- Undecidable properties of flat term rewrite systems (Q734041) (← links)
- CHAP and rewrite components (Q766175) (← links)
- Non-disjoint combined unification and closure by equational paramodulation (Q831919) (← links)
- The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem (Q843609) (← links)
- Coq formalization of the higher-order recursive path ordering (Q843949) (← links)
- KBO orientability (Q846165) (← links)
- Mechanically proving termination using polynomial interpretations (Q851142) (← links)
- Ordinal arithmetic: Algorithms and mechanization (Q851144) (← links)
- Cones and foci: A mechanical framework for protocol verification (Q853730) (← links)
- An effective proof of the well-foundedness of the multiset path ordering (Q857884) (← links)
- Tool-assisted specification and verification of typed low-level languages (Q861687) (← links)
- Formal correctness of a quadratic unification algorithm (Q877825) (← links)
- Elimination transformations for associative-commutative rewriting systems (Q877834) (← links)
- Mechanizing and improving dependency pairs (Q877836) (← links)
- The disconnection tableau calculus (Q877889) (← links)
- A new generic scheme for functional logic programming with constraints (Q880985) (← links)
- Differential (Lie) algebras from a functorial point of view (Q895968) (← links)
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\). (Q928657) (← links)
- Loop detection in term rewriting using the eliminating unfoldings (Q944383) (← links)
- Adding constants to string rewriting (Q945008) (← links)
- Normalization properties for shallow TRS and innermost rewriting (Q964737) (← links)
- Termination of narrowing via termination of rewriting (Q969619) (← links)
- MetiTarski: An automatic theorem prover for real-valued special functions (Q972422) (← links)