Automatic decidability

We give a set of inference rules with constant constraints. Then we show how to extend a set of equational clauses, so that if the application of these inference rules halts on these clauses, then the theory is decidable by applying a standard set of Paramodulation inference rules. In addition, we can determine the number of clauses generated in this decision procedure. For some theories, such as the theory of lists, there are 0(n × lg(n)) clauses. For others it is polynomial. And for others it is simply exponential such as the theory of (extensional) arrays.