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.
Recommendations
- Operational semantics of resolution and productivity in Horn clause logic
- Typed SLD-resolution: dynamic typing for logic programming
- A Proof-Theoretic Approach to Logic Programming. I. Clauses as Rules
- Proof relevant corecursive resolution
- Horn clause programs with polymorphic types: Semantics and resolution
Cites work
Cited in
(11)- Resolution and type theory
- Logic programming: laxness and saturation
- Coinductive soundness of corecursive type class resolution
- Operational semantics of resolution and productivity in Horn clause logic
- Executable relational specifications of polymorphic type systems using Prolog
- Proof relevant corecursive resolution
- scientific article; zbMATH DE number 5872252 (Why is no real title available?)
- Proof-relevant Horn clauses for dependent type inference and term synthesis
- scientific article; zbMATH DE number 5173934 (Why is no real title available?)
- Category theoretic semantics for theorem proving in logic programming: embracing the laxness
- Typed SLD-resolution: dynamic typing for logic programming
This page was built for publication: A type-theoretic approach to resolution
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5743587)
