Deciding the Word Problem in the Union of Equational Theories

Franz BaaderFranz Baader, Cesare TinelliCesare Tinelli

Datei:Baader-Tinelli-UIUCDCS-R-98-2073.ps.gz

Download

Franz Baader, Cesare Tinelli
Deciding the Word Problem in the Union of Equational Theories
Technical Report, Department of Computer Science, University of Illinois at Urbana-Champaign, volume UIUCDCS-R-98-2073, 1998. {UIUCDCS}-Report

Details
Bibtex

KurzfassungAbstract
The main contribution of this report 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. In addition, we show that---contrary to a common belief---the Nelson-Oppen combination method cannot be used to combine decision procedures for the word problem, even in the case of equational theories with disjoint signatures.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@techreport{ Baader-Tinelli-UIUCDCS-R-98-2073,
  author = {F. {Baader} and C. {Tinelli}},
  institution = {Department of Computer Science, University of Illinois at Urbana-Champaign},
  number = {UIUCDCS-R-98-2073},
  title = {Deciding the Word Problem in the Union of Equational Theories},
  type = {{UIUCDCS}-Report},
  year = {1998},
}