Uniform Derivation of Decision Procedures by Superposition
- 30 August 2001
- book chapter
- Published by Springer Nature
- p. 513-527
- https://doi.org/10.1007/3-540-44802-0_36
Abstract
No abstract availableKeywords
This publication has 11 references indexed in Scilit:
- A decision procedure for an extensional theory of arraysPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Paramodulation-Based Theorem ProvingPublished by Elsevier ,2001
- Abstract Congruence Closure and SpecializationsPublished by Springer Nature ,2000
- Congruence Closure Modulo Associativity and CommutativityPublished by Springer Nature ,2000
- Rewrite-based Equational Theorem Proving with Selection and SimplificationJournal of Logic and Computation, 1994
- THE WORD PROBLEM OF ACD-GROUND THEORIES IS UNDECIDABLEInternational Journal of Foundations of Computer Science, 1992
- Any ground associative-commutative theory has a finite canonical systemPublished by Springer Nature ,1991
- Rewrite SystemsPublished by Elsevier ,1990
- Fast Decision Procedures Based on Congruence ClosureJournal of the ACM, 1980
- Simple Word Problems in Universal Algebras††The work reported in this paper was supported in part by the U.S. Office of Naval Research.Published by Elsevier ,1970