A New Approach for Combining Decision Procedures for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method

Franz BaaderFranz Baader, Cesare TinelliCesare Tinelli

Datei:Baader-Tinelli-LTCS-96.ps.gz

Download

Franz Baader, Cesare Tinelli
A New Approach for Combining Decision Procedures for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method
Technical Report, LuFg Theoretical Computer Science, RWTH Aachen, volume LTCS-96-01, 1996. LTCS-Report

Details
Bibtex

KurzfassungAbstract
The Nelson-Oppen combination method can be used to combine decision procedures for the validity of quantifier-free formulae in first-order theories with disjoint signatures, provided that the theories to be combined are stably infinite. We show that, even though equational theories need not satisfy this property, Nelson and Oppen's method can be applied, after some minor modifications, to combine decision procedures for the validity of quantifier-free formulae in equational theories. Unfortunately, and contrary to a common belief, the method cannot be used to combine decision procedures for the word problem. We present a method that solves this kind of combination problem. Our method is based on transformation rules and also applies to equational theories that share a finite number of constant symbols.
Bemerkung: Note: An abridged version has appeared in Proc. CADE'97, Springer LNAI 1249.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@techreport{ Baader-Tinelli-LTCS-96,
  author = {F. {Baader} and C. {Tinelli}},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen},
  note = {An abridged version has appeared in Proc.\ CADE'97, Springer LNAI 1249.},
  number = {LTCS-96-01},
  title = {A New Approach for Combining Decision Procedures for the Word Problem, and Its Connection to the {Nelson-Oppen} Combination Method},
  type = {LTCS-Report},
  year = {1996},
}