The efficiency of finding a theorem of a first-order theory

33 Views Asked by At

First-order theories are semi-decidable since there is an algorithm allowing to deduce a given theorem applying inference rules. I'm interested in the efficiency of this algorithm, i.e., given a theorem, how fast the algorithm says we have a theorem. Is it NP, or more complex? Also, for what theories (say, group theory or number theory) the efficiency could/couldn't be improved?