Book chapter
A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
Automated Deduction—CADE-14, pp.19-33
Lecture Notes in Computer Science, Springer Berlin Heidelberg
06/08/2005
DOI: 10.1007/3-540-63104-6_3
Abstract
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.
Details
- Title: Subtitle
- A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
- Creators
- Franz Baader - RWTH Aachen UniversityCesare Tinelli - University of Illinois Urbana-Champaign
- Resource Type
- Book chapter
- Publication Details
- Automated Deduction—CADE-14, pp.19-33
- Publisher
- Springer Berlin Heidelberg; Berlin, Heidelberg
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/3-540-63104-6_3
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 06/08/2005
- Academic Unit
- Computer Science
- Record Identifier
- 9984259502302771
Metrics
7 Record Views