Sequent Calculi and Indexed Categories as a Foundation for Logic Programming. PhD Thesis, Dipartimento di Informatica

We present a semantic framework for sequent calculi which allows us to reason about properties of proofs. Using this framework we try to reconcile the proof theoretic approach to logic programming, essentially based on the concept of uniform proof, with the older model theoretic approach. Using abstract interpretation to model abstractions of proofs, we are able to port well known results for pure logic programming, in the field of abstract debugging and analysis, to richer languages such as hereditary Harrop formulas. While this approach is based on proof theory, there are cases of languages, like CLP, where models play a fundamental role. Therefore, we also propose a categorical semantic framework which is able to cope with both the syntax, the operational semantics and the model theory of a broad range of logic languages. A program is interpreted in an indexed category such that the base category contains all the possible states which can occur during the execution of the program (such as global constraints or type informations), while each fiber encodes the corresponding relevant logical properties. We define appropriate notions of categorical resolution and models, and we prove the related correctness and completeness properties.