undecidable

The first-order procedure SP differs from the proposi- tional procedure CP°₁ in an essential feature. Namely, CP°₁ always terminates while SP may run forever as we have seen with the example immediately after (3.7). This is not a specific defect of SP. Rather it is known that first-order logic is an undecidable theory while propositional logic is a decidable theory. This means that for the latter there are decision pro- cedures which for any formula decide whether it is valid or not — and CP°₁ in fact is such a decision procedure — while for the former such decision procedures do not exist in princi- ple. Thus SP, according to these results for which the reader is referred to any logic texts such as [End], [DrG] or [Lew], is of the kind which we may expect, it is a semi-decision procedure which confirms if a formula is valid but may run forever for invalid formulas. Therefore, termination by running out of time or space after any finite number of steps will leave the question for the validity of a formula unsettled. [...]

1982, Wolfgang Bibel, Automated Theorem Proving, Braunschweig: Friedr. Vieweg & Sohn, →ISBN, page 83