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?
Algorithm for enumerating theorems of first-order theories besides resolution
1
$\begingroup$
algorithms
logic
automated-theorem-proving
-
0Since 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
-
0I 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
-
0That would all but amount to restricting yourself to a _single_ enumeration algorithm (and minor uninteresting variants of the same). – 2011-12-28
-
0Ok, I give up. How do I ask my question without an unforgivable lack of rigor? – 2011-12-28
-
0I 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
-
0Given 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