A rewriting approach to satisfiability procedures ?
We show how a well-known superposition-based inference system for first-order equational logic can be used almost directly for deciding satisfiability in various theories including lists, encryption, extensional arrays, extensional finite sets, and combinations of them. We also give a superposition-based decision procedure for homomorphism.
equational logic lists encryption decision procedures homomorphism automated deduction term rewriting superposition arrays with extensionality finite sets with extensionality