A Type-Theoretic Approach to Resolution

TL;DR

This paper introduces a novel type-theoretic framework for logic programming, transforming Horn formulas into types and derivations into proof-terms, enabling proof evidence computation during resolution.

Contribution

It presents a new type-theoretic approach to SLD-resolution, linking logic programming with type theory, and introduces program transformations for proof evidence computation.

Findings

Applicable to structural resolution productivity theory

Enables proof evidence computation during derivations

Facilitates type class inference in logic programming

Abstract

We propose a new type-theoretic approach to SLD-resolution and Horn-clause logic programming. It views Horn formulas as types, and derivations for a given query as a construction of the inhabitant (a proof-term) for the type given by the query. We propose a method of program transformation that allows to transform logic programs in such a way that proof evidence is computed alongside SLD-derivations. We discuss two applications of this approach: in recently proposed productivity theory of structural resolution, and in type class inference.