Proof-Theoretic Characterisations of Logic Programming
James H. AndrewsAbstract: 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
Previous | Index | Next