Deciding the word problem in the union of equational theories.

DOI10.1006/inco.2001.3118zbMath1049.03032OpenAlexW2030179532WikidataQ57383722 ScholiaQ57383722MaRDI QIDQ1400706

Franz Baader, Cesare Tinelli

Publication date: 2002

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/afcaf72575104babba2c546de1d81a073028b49e

zbMATH Keywords

equational reasoningdecision procedure

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Word problems, etc. in computability and recursion theory (03D40) Equational classes, universal algebra in model theory (03C05)

Related Items

Combining word problems through rewriting in categories with products, Deciding the word problem in the union of equational theories., A new combination procedure for the word problem that generalizes fusion decidability results in modal logics, Decidability and combination results for two notions of knowledge in security protocols, Automated verification of selected equivalences for security protocols, Canonization for disjoint unions of theories, Model-theoretic methods in combined constraint satisfiability, On Hierarchical Reasoning in Combinations of Theories, Unions of non-disjoint theories and combinations of satisfiability procedures

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unification in a combination of arbitrary disjoint equational theories
• Counterexamples to termination for the direct sum of term rewriting systems
• Combination of constraint solvers for free and quasi-free structures
• Combining symbolic constraint solvers on algebraic domains
• Combining word problems through rewriting in categories with products
• Deciding the word problem in the union of equational theories.
• Unions of non-disjoint theories and combinations of satisfiability procedures
• Modular properties of composable term rewriting systems
• Completion of a Set of Rules Modulo a Set of Equations
• Proving termination with multiset orderings
• Fast Decision Procedures Based on Congruence Closure
• Simplification by Cooperating Decision Procedures
• An Efficient Unification Algorithm
• The join of equational theories
• Term Rewriting and All That
• On the Church-Rosser property for the direct sum of term rewriting systems
• A Machine-Oriented Logic Based on the Resolution Principle