First Order Logic and undecidability

Question

I've read that the resolution procedure (that derives from the Resolution Rule) is complete. So if there exist an empty clause, the procedure finds it.

But , what about undecidability ? Does the resolution procedure suffer of it ?

Answer 1

Well, it might. If you apply the resolution procedure to a theory that is undecidable, then obviously you'll run into trouble. Even if the theory is axiomatizable, it may simply not be complete, and then of course certain propositions will remain undecidable.