Polymorphic lemmas and definitions in λProlog and Twelf

Andrew W. Appel, Amy P. Felty

Research output: Contribution to journalArticle

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 languageEnglish (US)
Pages (from-to)1-39
Number of pages39
JournalTheory and Practice of Logic Programming
Volume4
Issue number1-2
DOIs
StatePublished - Jan 1 2004

All Science Journal Classification (ASJC) codes

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

Keywords

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

Fingerprint Dive into the research topics of 'Polymorphic lemmas and definitions in λProlog and Twelf'. Together they form a unique fingerprint.

  • Cite this