A computational task that for each possible input requires “true” or “false” to be output, depending on whether the input possesses a certain property. An algorithm that produces the correct decision in each case is called a decision procedure for that problem. If a decision procedure exists then the problem is said to be (algorithmically) solvable, while an (algorithmically) unsolvable problem is one for which no decision procedure exists. An example is logical validity, the inputs being logical expressions, with the output “true” for valid expressions and “false” for others. This problem is solvable for propositional logic (the construction of truth tables being a decision procedure) but not for predicate logic (by Church's theorem of 1936). Solvable problems can be further classified according to the efficiency of decision procedures existing for them (see P—NP question).
Some unsolvable problems possess a semidecision procedure, i.e. an algorithm that correctly outputs “true” but fails to terminate in cases where “false” should be output. This is the same as saying that the inputs requiring the output “true” form a set that is recursively enumerable (but need not be recursive). Alternatively one can say that the problem corresponds to a predicate that is semidecidable (but need not be decidable).