## Logic Programming via Proof-Valued Computations

**David J Pym and Lincoln A Wallen**
*Abstract:* We argue that the computation of a logic
program can be usefully divided into two distinct phases: the first
being a proof-valued computation or proof-search; the second a
residual computation, or answer extraction. Extension of extraction
techniques to various theories then permits more extensive
languages and proof procedures to be employed for the computational
solution of problems.

We illustrate these ideas with a simple propositional logic and
show that SLD-resolution computes presentations of proofs in which
the residual computation may be interleaved with the proof-search,
whereas a more general proof procedure yields shorter presentations
of (the same) proofs, but which require more extensive residual
computations.

*LFCS report ECS-LFCS-92-246*

Previous |

Index |

Next