A type-theoretic approach to resolution

Research output: Chapter in Book/Report/Conference proceedingChapter

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.

LanguageEnglish
Title of host publicationLogic-Based Program Synthesis and Transformation
Subtitle of host publication25th International Symposium, LOPSTR 2015, Siena, Italy, July 13-15, 2015. Revised Selected Papers
EditorsMoreno Falaschi
PublisherSpringer International Publishing
Pages91-106
Number of pages16
ISBN (Electronic)9783319274362
ISBN (Print)9783319274355
DOIs
Publication statusPublished - 2015

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
Volume9527
ISSN (Print)0302-9743

Fingerprint

Logic programming
Productivity

Keywords

  • Logic programming
  • Typed lambda calculus
  • Realizability transformation
  • Reduction systems
  • Structural resolution

Cite this

Fu, P., & Komendantskaya, E. (2015). A type-theoretic approach to resolution. In M. Falaschi (Ed.), Logic-Based Program Synthesis and Transformation: 25th International Symposium, LOPSTR 2015, Siena, Italy, July 13-15, 2015. Revised Selected Papers (pp. 91-106). (Lecture Notes in Computer Science; Vol. 9527). Springer International Publishing. https://doi.org/10.1007/978-3-319-27436-2_6
Fu, Peng ; Komendantskaya, Ekaterina. / A type-theoretic approach to resolution. Logic-Based Program Synthesis and Transformation: 25th International Symposium, LOPSTR 2015, Siena, Italy, July 13-15, 2015. Revised Selected Papers. editor / Moreno Falaschi. Springer International Publishing, 2015. pp. 91-106 (Lecture Notes in Computer Science).
@inbook{391fdc7c83214989a44ae6ada7f71084,
title = "A type-theoretic approach to resolution",
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.",
keywords = "Logic programming, Typed lambda calculus, Realizability transformation, Reduction systems, Structural resolution",
author = "Peng Fu and Ekaterina Komendantskaya",
year = "2015",
doi = "10.1007/978-3-319-27436-2_6",
language = "English",
isbn = "9783319274355",
series = "Lecture Notes in Computer Science",
publisher = "Springer International Publishing",
pages = "91--106",
editor = "Moreno Falaschi",
booktitle = "Logic-Based Program Synthesis and Transformation",
address = "Switzerland",

}

Fu, P & Komendantskaya, E 2015, A type-theoretic approach to resolution. in M Falaschi (ed.), Logic-Based Program Synthesis and Transformation: 25th International Symposium, LOPSTR 2015, Siena, Italy, July 13-15, 2015. Revised Selected Papers. Lecture Notes in Computer Science, vol. 9527, Springer International Publishing, pp. 91-106. https://doi.org/10.1007/978-3-319-27436-2_6

A type-theoretic approach to resolution. / Fu, Peng; Komendantskaya, Ekaterina.

Logic-Based Program Synthesis and Transformation: 25th International Symposium, LOPSTR 2015, Siena, Italy, July 13-15, 2015. Revised Selected Papers. ed. / Moreno Falaschi. Springer International Publishing, 2015. p. 91-106 (Lecture Notes in Computer Science; Vol. 9527).

Research output: Chapter in Book/Report/Conference proceedingChapter

TY - CHAP

T1 - A type-theoretic approach to resolution

AU - Fu, Peng

AU - Komendantskaya, Ekaterina

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

KW - Logic programming

KW - Typed lambda calculus

KW - Realizability transformation

KW - Reduction systems

KW - Structural resolution

U2 - 10.1007/978-3-319-27436-2_6

DO - 10.1007/978-3-319-27436-2_6

M3 - Chapter

SN - 9783319274355

T3 - Lecture Notes in Computer Science

SP - 91

EP - 106

BT - Logic-Based Program Synthesis and Transformation

A2 - Falaschi, Moreno

PB - Springer International Publishing

ER -

Fu P, Komendantskaya E. A type-theoretic approach to resolution. In Falaschi M, editor, Logic-Based Program Synthesis and Transformation: 25th International Symposium, LOPSTR 2015, Siena, Italy, July 13-15, 2015. Revised Selected Papers. Springer International Publishing. 2015. p. 91-106. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-27436-2_6