scientific article; zbMATH DE number 3299786

Cited in

(only showing first 100 items - show all)

Proving Confluence of Term Rewriting Systems Automatically
Using forcing to prove completeness of resolution and paramodulation
Reduction operators and completion of rewriting systems
On graph rewritings
Unique normal forms for nonlinear term rewriting systems: Root overlaps
Optimization by non-deterministic, lazy rewriting
Theorem proving with group presentations: examples and questions
About the rewriting systems produced by the Knuth-Bendix completion algorithm
String diagram rewrite theory III: Confluence with and without Frobenius
Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study
Reduction relations for monoid semirings
On fairness of completion-based theorem proving strategies
AC-complete unification and its application to theorem proving
The first-order theory of one-step rewriting is undecidable
Automatic acquisition of search control knowledge from multiple proof attempts.
The undecidability of the first-order theories of one step rewriting in linear canonical systems
Completion of first-order clauses with equality by strict superposition
More efficient left-to-right matching for overlapping pattern
An efficient representation of arithmetic for term rewriting
Termination tools in ordered completion
On the essence and initiality of conflicts in \(\mathcal{M} \)-adhesive transformation systems
Critical pairs in term graph rewriting
Complete demodulation for automatic theorem proving
Integration of parametric and ``ad hoc second order polymorphism in a calculus with subtyping
Deductive and inductive synthesis of equational programs
More efficient bottom-up multi-pattern matching in trees
On weakly confluent monadic string-rewriting systems
Solving divergence in Knuth--Bendix completion by enriching signatures
Using geometric rewrite rules for solving geometric problems symbolically
The problem of demodulator adjunction
High-Level Theories
Conjecture synthesis for inductive theories
Term rewriting induction
Improving associative path orderings
Rewrite method for theorem proving in first order theory with equality
Algebraic databases
Iterating transducers
Confluence by critical pair analysis revisited
A posthumous contribution by Larry Wos: excerpts from an unpublished column
Larry Wos: visions of automated reasoning
Set of support, demodulation, paramodulation: a historical perspective
Disjunctive bases of applied algebras of sets and their use in problems of combinatorial geometry
A superposition oriented theorem prover
Simple termination of rewrite systems
Some results on the confluence property of combined term rewriting systems
On equational theories, unification, and (un)decidability
Thue systems as rewriting systems
A list of applications of Stallings automata
Implementing first-order rewriting with constructor systems
scientific article; zbMATH DE number 3684923 (Why is no real title available?)
Shuffle polygraphic resolutions for operads
Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
Meta-rule synthesis from crossed rewrite systems
Rewriting with a nondeterministic choice operator
Analysis of Dehn's algorithm by critical pairs
Logic programs with equational type specifications
Operational semantics of a kernel of the language ELECTRE
PATCH graphs: an efficient data structure for completion of finitely presented groups
Rewriting with generalized nominal unification
Decision problems for finite special string-rewriting systems that are confluent on some congruence class
Undecidable properties of monoids with word problem solvable in linear time. II: Cross sections and homological and homotopical finiteness conditions.
Undecidable properties of monoids with word problem solvable in linear time.
Conditional congruence closure over uninterpreted and interpreted symbols
Weakly-non-overlapping non-collapsing shallow term rewriting systems are confluent
Multiagent temporal logics, unification problems, and admissibilities
Completion for rewriting modulo a congruence
Complete sets of transformations for general E-unification
scientific article; zbMATH DE number 3821100 (Why is no real title available?)
Conditional rewrite rule systems with built-in arithmetic and induction
Termination proofs and the length of derivations
String rewriting for double coset systems.
Higher-order proof by consistency
Pregeometric spaces from Wolfram model rewriting systems as homotopy types
Invariants, patterns and weights for ordering terms
Complete sets of reductions with constraints
On restrictions of ordered paramodulation with simplification
Set-theoretic graph rewriting
Complete equational unification based on an extension of the Knuth-Bendix completion procedure
Using the tree representation of terms to recognize matching with neural networks
Proving group isomorphism theorems
A refinement of strong sequentiality for term rewriting with constructors
Automatic Termination
Term orderings for non-reachability of (conditional) rewriting
Canonical ground Horn theories
Unification and Inference Rules in the Multi-modal Logic of Knowledge and Linear Time LTK
Automatic inductive theorem proving using Prolog
scientific article; zbMATH DE number 40567 (Why is no real title available?)
Unification theory
Any ground associative-commutative theory has a finite canonical system
Rippling: A heuristic for guiding inductive proofs
Implementing contextual rewriting
Calcul de longueurs de chaînes de réécriture dans le monoïde libre
On using ground joinable equations in equational theorem proving
Algebraic structures of \(F\)-manifolds via pre-Lie algebras
Schematization of infinite sets of rewrite rules generated by divergent completion processes
Confluence and commutation for nominal rewriting systems with atom-variables
Ordered rewriting and confluence
Normalising Lustre preserves security
Boolean algebra admits no convergent term rewriting system
Coherent confluence modulo relations and double groupoids

This page was built for publication:

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