## Proof-Theoretic Characterisations of Logic Programming

**James H. Andrews**
*Abstract:* A characterisation of a logic programming
system is given in the form of a natural deduction proof system.
The proof system is proven to be ``equivalent'' to an operational
semantics for the logic programming system, in the sense that the
set of theorems of the proof system is exactly the set of
existential closures of queries solvable in the operational
semantics. It is argued that this proof-theoretic characterisation
captures our intuitions about logic programming better than do
traditional characterisations, such as those using resolution
or

*ECS-LFCS-89-77*

Previous |

Index |

Next