Proof and Computation

Solving Problems is Hard .. so we may need to use algorithms which are powerful, even if not wholly reliable. Perhaps even neural nets or other AI techniques. This is OK if .. Checking Solutions is Easy .. if reliable algorithms suffice to check a solution, so that any mistakes can be weeded out. This gives us a route to combining.. Power and Assurance .. wherever we have an effective decision procedure for the adequacy of solutions. 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. Logic for Problem Solving When problems are formally described in first order logic, powerful general proof techniques such as resolution may be used to obtain solutions. An attempt to prove the existence of a solution proceeds by attempting to derive a contradiction from the denial that a solution exists. If successful a solution to the problem can be extracted from the proof. 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.

The LCF Paradigm Where machines are involved in proof the LCF paradigm is valuable. This provides a method for implementing proof checking which supports flexible proof search programming 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. Programs from Proofs Constructive logical systems, which are particularly aligned to computation, provide a framework in which proof of the consistency of a specification yields a program meeting the specification. Logic Programming 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.

© created 1996/8/22 modified 1996/12/23