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

Franz Baader, Cesare Tinelli
A New Approach for Combining Decision Procedures for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method
In W. McCune, eds., Proceedings of the 14th International Conference on Automated Deduction (CADE-97), volume 1249 of Lecture Notes in Artificial Intelligence, 19-33, 1997. Springer

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.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ Baader-Tinelli-CADE-97,
  author = {F. {Baader} and C. {Tinelli}},
  booktitle = {Proceedings of the 14th International Conference on Automated Deduction (CADE-97)},
  editor = {W. {McCune}},
  pages = {19--33},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Artificial Intelligence},
  title = {A New Approach for Combining Decision Procedures for the Word Problem, and Its Connection to the {Nelson-Oppen} Combination Method},
  volume = {1249},
  year = {1997},
}