A type-theoretic approach to resolution

Peng Fu; Ekaterina Komendantskaya

doi:10.1007/978-3-319-27436-2_6

A type-theoretic approach to resolution

Peng Fu, Ekaterina Komendantskaya

Research output: Chapter in Book/Report/Conference proceeding › Chapter

4 Citations (Scopus)

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.

Original language	English
Title of host publication	Logic-Based Program Synthesis and Transformation
Subtitle of host publication	25th International Symposium, LOPSTR 2015, Siena, Italy, July 13-15, 2015. Revised Selected Papers
Editors	Moreno Falaschi
Publisher	Springer
Pages	91-106
Number of pages	16
ISBN (Electronic)	9783319274362
ISBN (Print)	9783319274355
DOIs	https://doi.org/10.1007/978-3-319-27436-2_6
Publication status	Published - 2015

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer International Publishing
Volume	9527
ISSN (Print)	0302-9743

Keywords

Logic programming
Typed lambda calculus
Realizability transformation
Reduction systems
Structural resolution

Access to Document

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

http://www.scopus.com/inward/record.url?scp=84952785035&partnerID=8YFLogxK

Cite this

@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",

pages = "91--106",

editor = "Moreno Falaschi",

booktitle = "Logic-Based Program Synthesis and Transformation",

}

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, 2015. p. 91-106 (Lecture Notes in Computer Science; Vol. 9527).

Research output: Chapter in Book/Report/Conference proceeding › Chapter

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

ER -

A type-theoretic approach to resolution

Abstract

Publication series

Keywords

Access to Document

Fingerprint

Cite this