Formal logical systems provide a framework within which powerful techniques can reliably be applied. They permit advanced and possibly unreliable problem solving techniques to be safely applied. Though such general proof techniques are limited in their value and must in practice be supplemented by a range of more specific techniques, the integration of problem solving with proof methods can still be sustained. |
In the LCF paradigm proofs are not textual structures terminating in the proven theorem, they are computations which yield the theorem. The course of the computation is constrained in ways which closely relate to admissible inferences in the logic so that any computation will yield only theorems however exotic the algorithms employed. Though general proof search methods can be used for problem solving they prove to be too inefficient for most problems. By restricting the problem statement to first order horn clauses it is possible to control the search path of the theorem prover and improve efficiency. By developing languages in a rather pragmatic way from this starting point, logic programming languages were devised which permitted a more or less logical description of a problem to guide the search for solutions. |