Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
Since there are in general infinitely many theorems, how do you propose to measure "time complexity"? If you're simply counting amortized effort per new theorem printed, you could write a very fast generator of new propositional tautologies and dovetail that together with your favorite but slow enumeration of all theorems. – Henning Makholm Dec 28 '11 at 21:26
I could specify a particular order that theorems must be enumerated in. I'm not doing so because that would technically exclude possible algorithms I am still interested in. – user21395 Dec 28 '11 at 21:32
That would all but amount to restricting yourself to a single enumeration algorithm (and minor uninteresting variants of the same). – Henning Makholm Dec 28 '11 at 21:36
Ok, I give up. How do I ask my question without an unforgivable lack of rigor? – user21395 Dec 28 '11 at 21:49
I don't know. I doubt it is possible at all to make what you're attempting precise without opening loopholes that makes the formalization uninteresting. – Henning Makholm Dec 28 '11 at 22:06

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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.