An Adjunction-Theoretic Foundation for Proof Search in Intuitionistic First-Order Categorical Logic Programming

Document
Document

In this thesis we compose a proof-theoretic approach to logic programming with a category-theoretic approach to proof theory. This allows us to present the computation mechanisms of several systems of logic programming as proof search strategies within an intuitionistic first-order sequent calculus with logic variables and to analyze aspects of their behavior algebraically. Beginning from the basic categorical construction of an adjunction, we present Gentzen's formal derivation system of natural deduction for intuitionistic first-order logic as a categorical graphical language, in which equivalence classes of derivations under the usual relations of convertibility correspond precisely to arrows in a freelygenerated hyperdoctrine categorical semantics. We show that the inference rules and conversion relations on derivations have uniform adjoint-theoretic interpretations, and that the connectives are naturally partitioned into two chiral classes, depending on whether they are characterized by a right or a left adjoint functor. We observe that the adjoint-theoretic descriptions of the non-invertible rules for quantifiers each decompose their natural deduction counterpart into a purely logical rule and a substitution. By using the same categorical semantics for the formal derivation system of sequent calculus, we are able present a version in which the generic parameters, logic variables and substitutions of logic programming are given first-class status. This in turn allows us to present the operational semantics of SLD-resolution for Horn logic (the logic underlying the programming language Prolog), and that of uniform proof for hereditarily Harrop logic (the first-order fragment of the logic underlying the programming language λ-Prolog), as search strategies in this sequent calculus. We show that the adjoint-theoretic description of the connectives permits a natural extension of the strategy of uniform proof to a syntactically richer language, which we call the language of constructive sequents. We adopt Andreoli's idea of focused proof search from linear logic as a search strategy for intuitionistic logic within our sequent system, where it becomes a natural generalization of the strategy of uniform proof. We show that one of the two principles underlying focusing is immediately justified by the adjoint-theoretic properties of the connectives. We compare this focused proof search strategy with a different one proposed by Dyckhoff and Pinto in the context of the input-output semantics of logic programming.

    Item Description
    Name(s)
    Thesis advisor: Lipton, James
    Date
    April 01, 2013
    Extent
    168 pages
    Language
    eng
    Genre
    Physical Form
    electronic
    Rights and Use
    In Copyright – Non-Commercial Use Permitted
    Digital Collection
    PID
    ir:2254