Deciding the word problem in the union of equational theories.
type: Item
instance of: scholarly article
title: Deciding the word problem in the union of equational theories.
zbMATH Open document ID: 1049.03032
author: Franz Baader
author: Cesare Tinelli
published in: Information and Computation
publication date: 2002-01-01T00:00:00Z
Mathematics Subject Classification ID: 03D40
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03C05
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68Q42
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 1964170
zbMATH Keywords: equational reasoning
zbMATH Keywords: decision procedure
MaRDI profile type: Publication
OpenAlex ID: W2030179532
Wikidata QID: Q57383722
cites work: Term Rewriting and All That
cites work: Combination of constraint solvers for free and quasi-free structures
cites work: Q4518874
cites work: Q4938605
cites work: Proving termination with multiset orderings
cites work: Combining word problems through rewriting in categories with products
cites work: Completion of a Set of Rules Modulo a Set of Equations
cites work: Combining symbolic constraint solvers on algebraic domains
cites work: An Efficient Unification Algorithm
cites work: Q5583066
cites work: Simplification by Cooperating Decision Procedures
cites work: Fast Decision Procedures Based on Congruence Closure
cites work: Modular properties of composable term rewriting systems
cites work: The join of equational theories
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Unification in a combination of arbitrary disjoint equational theories
cites work: Q3030272
cites work: Q4385439
cites work: Unions of non-disjoint theories and combinations of satisfiability procedures
cites work: Counterexamples to termination for the direct sum of term rewriting systems
cites work: On the Church-Rosser property for the direct sum of term rewriting systems
DBLP publication ID: journals/iandc/BaaderT02
DOI: 10.1006/INCO.2001.3118
Recommended article: Q4938605
Recommended article: On a connection between the word problem and decidability of the equational theory
Recommended article: Q3028369
Recommended article: Q3779785
Recommended article: The satisfiability of word equations: decidable and undecidable theories
Recommended article: Unification problem in equational theories
Recommended article: On equational theories, unification, and (un)decidability
Recommended article: A finitely axiomatizable undecidable equational theory with recursively solvable word problems
Recommended article: Unification in the union of disjoint equational theories: Combining decision procedures
Recommended article: Term Rewriting and Applications
description: scientific article; zbMATH DE number 1964170