Algorithm for enumerating theorems of first-order theories besides resolution

Question

Is there a general algorithm for enumerating the theorems of any finite first-order theory with a better time complexity than simply using resolution on all first-order logic formulas?

Answer 1

First, you cannot use resolution to enumerate all theorems. Resolution is only refutationally complete: it always derives an empty clause from a contradictory set of formulas it it. But it will not derive all possible theorems from a set of formulas. This is one of the things that makes resolution much faster than just enumerating all possible theorems. (Another thing that makes is fast is that it uses most general unifications. This way it avoids making unnecessary substitutions.)

Enumerating all first order theorems is simple. You start with the set of axioms of a given theory and repeat applying the inference rules. As mentioned in the comments, it's not possible to talk about time complexity, because the process never ends. Any two procedures that produce all theorems and don't print duplicates will be equivalent. They only differ in the order in which the theorems are enumerated. You need to specify some additional constraint that will make the process finite (like find all theorems shorter than n). Or specify how to compare two procedures that enumerate all theorems.

The problem is most theorems in such an enumeration will be completely useless. There is no general criterion how to distinguish which theorems are "interesting", "useful", contain "a lot of knowledge" etc. If we had such criterion, we could aim at enumerating all "useful" or "interesting" theorems in a given theory.