scientific article; zbMATH DE number 3299786

Cited in

(only showing first 100 items - show all)

Gröbner-Shirshov basis for the braid group in the Birman-Ko-Lee generators.
Gröbner-Shirshov bases for associative algebras with multiple operators and free Rota-Baxter algebras.
Termination of narrowing revisited
Inductive proof search modulo
Some fundamental algebraic tools for the semantics of computation. I. Comma categories, colimits, signatures and theories
A superposition oriented theorem prover
Axiomatisation des tests
Rewrite systems on a lattice of types
Equational methods in first order predicate calculus
Conditional rewrite rules
Automated inferencing
Termination orderings for associative-commutative rewriting systems
A finite Thue system with decidable word problem and without equivalent finite canonical system
Pseudo-natural algorithms for the word problem for finitely presented monoids and groups
On sufficient-completeness and related properties of term rewriting systems
On merging software extensions
On recursive path ordering
Reductions in tree replacement systems
n-level rewriting systems
On solving the equality problem in theories defined by Horn clauses
The problems of cyclic equality and conjugacy for finite complete rewriting systems
A refinement of strong sequentiality for term rewriting with constructors
Proof by consistency
Rewriting with a nondeterministic choice operator
A catalogue of complete group presentations
Termination of rewriting
Rewrite method for theorem proving in first order theory with equality
Complexity of matching problems
Thue systems as rewriting systems
Unification in combinations of collapse-free regular theories
Analysis of Dehn's algorithm by critical pairs
Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study
The Church-Rosser property for ground term-rewriting systems is decidable
Simplifying conditional term rewriting systems: Unification, termination and confluence
Embedding Boolean expressions into logic programming
A class of confluent term rewriting systems and unification
On deciding the confluence of a finite string-rewriting system on a given congruence class
History and basic features of the critical-pair/completion procedure
Automatic inductive theorem proving using Prolog
Only prime superpositions need be considered in the Knuth-Bendix completion procedure
Critical pair criteria for completion
Computing a Gröbner basis of a polynomial ideal over a Euclidean domain
Implementing first-order rewriting with constructor systems
Pseudo-natural algorithms for finitely generated presentations of monoids and groups
A multi-level geometric reasoning system for vision
Finite generation of ambiguity in context-free languages
A geometrical approach to multiset orderings
Lifting canonical algorithms from a ring R to the ring R[x]
Fast Knuth-Bendix completion with a term rewriting system compiler
Higher-order rewrite systems and their confluence
A notation for lambda terms. A generalization of environments
A note on simplification orderings
New decision algorithms for finitely presented commutative semigroups
A complete proof of correctness of the Knuth-Bendix completion algorithm
Testing for the Church-Rosser property
A Noetherian and confluent rewrite system for idempotent semigroups
Rewrite, rewrite, rewrite, rewrite, rewrite, \dots
Completion for unification
Fuzzy term-rewriting system
What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory
A new approach to recursion removal
Semantics of order-sorted specifications
A criterion for proving noetherianity of a relation
Some experiments with a completion theorem prover
The Knuth-Bendix procedure for strings as a substitute for coset enumeration
Operational semantics of a kernel of the language ELECTRE
New methods for using Cayley graphs in interconnection networks
Termination and completion modulo associativity, commutativity and identity
Confluent linear numeration systems
How to decide the lark
The diamond lemma for ring theory
Non-resolution theorem proving
Complete demodulation for automatic theorem proving
Free distributive groupoids
Completion for rewriting modulo a congruence
Complete sets of transformations for general E-unification
Schematization of infinite sets of rewrite rules generated by divergent completion processes
Relating rewriting techniques on monoids and rings: congruences on monoids and ideals in monoid rings
The first-order theory of linear one-step rewriting is undecidable
The finiteness of finitely presented monoids
On Gröbner bases of noncommutative power series
Unification problem in equational theories
Deciding embeddability of partial groupoids into semigroups
Simplification orderings: Putting them to the test
Single axioms for groups and abelian groups with various operations
On the duality of abduction and model generation in a framework for model generation with equality
Generating polynomial orderings
Automated proofs of equality problems in Overbeek's competition
Rewriting systems of Coxeter groups
Deductive and inductive synthesis of equational programs
Proving termination of (conditional) rewrite systems. A semantic approach
Eta-conversion for the languages of explicit substitutions
Extending Bachmair's method for proof by consistency to the final algebra
Some results on the confluence property of combined term rewriting systems
Automated deduction with associative-commutative operators
A complete equational axiomatization for prefix iteration
The shortest single axioms for groups of exponent 4
Single identities for ternary Boolean algebras
Weights for total division orderings on strings
Buchberger's algorithm: The term rewriter's point of view

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)