1
$\begingroup$

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?

  • 0
    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.2011-12-28
  • 0
    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.2011-12-28
  • 0
    That would all but amount to restricting yourself to a _single_ enumeration algorithm (and minor uninteresting variants of the same).2011-12-28
  • 0
    Ok, I give up. How do I ask my question without an unforgivable lack of rigor?2011-12-28
  • 0
    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.2011-12-28
  • 0
    Given any sound and complete algorithm enumerating first order tautologies, you cannot have any computable function bounding the time that the algorithm will output the n-th theorem (w.r.t. any computable ordering of all formulas, i.e. a injective computable function that assigns a number to each formula).2011-12-30

1 Answers 1