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 (Lead / Corresponding author), Ekaterina Komendantskaya

Computing

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

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 International Publishing
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
Event	25th International Symposium on Logic-Based Program Synthesis and Transformation - University of Siena, Siena, Italy Duration: 13 Jul 2015 → 15 Jul 2015 http://alpha.diism.unisi.it/lopstr15/

Publication series

Name	Lecture notes in computer science
Publisher	Springer International Publishing
Volume	9527
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	25th International Symposium on Logic-Based Program Synthesis and Transformation
Abbreviated title	LOPSTR 2015
Country/Territory	Italy
City	Siena
Period	13/07/15 → 15/07/15
Internet address	http://alpha.diism.unisi.it/lopstr15/

Keywords

Logic programming
Realizability transformation
Reduction systems
Structural resolution
Typed lambda calculus

ASJC Scopus subject areas

General Computer Science
Theoretical Computer Science

Access to Document

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

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

@inproceedings{6875db5e7e724ce087bc4eca3e9428c1,

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, Realizability transformation, Reduction systems, Structural resolution, Typed lambda calculus",

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 = "Falaschi, {Moreno }",

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

address = "Switzerland",

note = " 25th International Symposium on Logic-Based Program Synthesis and Transformation , LOPSTR 2015 ; Conference date: 13-07-2015 Through 15-07-2015",

url = "http://alpha.diism.unisi.it/lopstr15/",

}

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, 25th International Symposium on Logic-Based Program Synthesis and Transformation , Siena, Italy, 13/07/15. https://doi.org/10.1007/978-3-319-27436-2_6

A type-theoretic approach to resolution. / Fu, Peng (Lead / Corresponding author); 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 proceeding › Conference contribution

TY - GEN

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 - Realizability transformation

KW - Reduction systems

KW - Structural resolution

KW - Typed lambda calculus

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

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

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

M3 - Conference contribution

AN - SCOPUS:84952785035

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

T2 - 25th International Symposium on Logic-Based Program Synthesis and Transformation

Y2 - 13 July 2015 through 15 July 2015

ER -

A type-theoretic approach to resolution

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Coalgebraic Logic Programming for Type Inference: Parallelism and Corecursion for New Generation of Programming Languages (Joint with the University of Bath)

Cite this

A type-theoretic approach to resolution

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Projects

Coalgebraic Logic Programming for Type Inference: Parallelism and Corecursion for New Generation of Programming Languages (Joint with the University of Bath)

Cite this