Deciding the Word Problem in the Union of Equational Theories

From International Center for Computational Logic

Toggle side column

Deciding the Word Problem in the Union of Equational Theories

Franz BaaderFranz Baader,  Cesare TinelliCesare Tinelli
Deciding the Word Problem in the Union of Equational Theories


Franz Baader, Cesare Tinelli
Deciding the Word Problem in the Union of Equational Theories
Information and Computation, 178(2):346-390, 2002
  • KurzfassungAbstract
    The main contribution of this article is a new method for combining decision procedures for the word problem in equational theories. In contrast to previous methods, it is based on transformation rules, and also applies to theories sharing "constructors."
  • Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory
@article{ BaaderTinelliIC02,
  author = {F. {Baader} and C. {Tinelli}},
  journal = {Information and Computation},
  number = {2},
  pages = {346--390},
  title = {Deciding the Word Problem in the Union of Equational Theories},
  volume = {178},
  year = {2002},
}