Polymorphic lemmas and definitions in λProlog and Twelf

Andrew W. Appel; Amy P. Felty

doi:10.1017/S1471068403001698

Polymorphic lemmas and definitions in λProlog and Twelf

Andrew W. Appel, Amy P. Felty

Research output: Contribution to journal › Article › peer-review

3 Scopus citations

Abstract

λProlog is known to be well-suited for expressing and implementing logics and inference systems. We show that lemmas and definitions in such logics can be implemented with a great economy of expression. We encode a higher-order logic using an encoding that maps both terms and types of the object logic (higher-order logic) to terms of the metalanguage (λProlog). We discuss both the Terzo and Teyjus implementations of λProlog. We also encode the same logic in Twelf and compare the features of these two metalanguages for our purposes.

Original language	English (US)
Pages (from-to)	1-39
Number of pages	39
Journal	Theory and Practice of Logic Programming
Volume	4
Issue number	1-2
DOIs	https://doi.org/10.1017/S1471068403001698
State	Published - 2004

All Science Journal Classification (ASJC) codes

Software
Artificial Intelligence
Theoretical Computer Science
Hardware and Architecture
Computational Theory and Mathematics

Keywords

Lambda Prolog
Twelf
definitions
higher-order logic programming
lemmas
logical frameworks
polymorphism
proof-carrying code
theorem proving

Access to Document

10.1017/S1471068403001698

Cite this

@article{4b8b915970af479b9104764b45391386,

title = "Polymorphic lemmas and definitions in λProlog and Twelf",

abstract = "λProlog is known to be well-suited for expressing and implementing logics and inference systems. We show that lemmas and definitions in such logics can be implemented with a great economy of expression. We encode a higher-order logic using an encoding that maps both terms and types of the object logic (higher-order logic) to terms of the metalanguage (λProlog). We discuss both the Terzo and Teyjus implementations of λProlog. We also encode the same logic in Twelf and compare the features of these two metalanguages for our purposes.",

keywords = "Lambda Prolog, Twelf, definitions, higher-order logic programming, lemmas, logical frameworks, polymorphism, proof-carrying code, theorem proving",

author = "Appel, {Andrew W.} and Felty, {Amy P.}",

year = "2004",

doi = "10.1017/S1471068403001698",

language = "English (US)",

volume = "4",

pages = "1--39",

journal = "Theory and Practice of Logic Programming",

issn = "1471-0684",

publisher = "Cambridge University Press",

number = "1-2",

}

TY - JOUR

T1 - Polymorphic lemmas and definitions in λProlog and Twelf

AU - Appel, Andrew W.

AU - Felty, Amy P.

PY - 2004

Y1 - 2004

N2 - λProlog is known to be well-suited for expressing and implementing logics and inference systems. We show that lemmas and definitions in such logics can be implemented with a great economy of expression. We encode a higher-order logic using an encoding that maps both terms and types of the object logic (higher-order logic) to terms of the metalanguage (λProlog). We discuss both the Terzo and Teyjus implementations of λProlog. We also encode the same logic in Twelf and compare the features of these two metalanguages for our purposes.

AB - λProlog is known to be well-suited for expressing and implementing logics and inference systems. We show that lemmas and definitions in such logics can be implemented with a great economy of expression. We encode a higher-order logic using an encoding that maps both terms and types of the object logic (higher-order logic) to terms of the metalanguage (λProlog). We discuss both the Terzo and Teyjus implementations of λProlog. We also encode the same logic in Twelf and compare the features of these two metalanguages for our purposes.

KW - Lambda Prolog

KW - Twelf

KW - definitions

KW - higher-order logic programming

KW - lemmas

KW - logical frameworks

KW - polymorphism

KW - proof-carrying code

KW - theorem proving

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

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

U2 - 10.1017/S1471068403001698

DO - 10.1017/S1471068403001698

M3 - Article

AN - SCOPUS:2142769727

SN - 1471-0684

VL - 4

SP - 1

EP - 39

JO - Theory and Practice of Logic Programming

JF - Theory and Practice of Logic Programming

IS - 1-2

ER -

Polymorphic lemmas and definitions in λProlog and Twelf

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this