Logic representation in LF

Robert Harper, Donald Sannella, Andrzej Tarlecki

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

The purpose of a logical framework such as LF is to provide a language for defining logical systems suitable for use in a logic-independent proof development environment. In previous work we have developed a theory of representation of logics in a logical framework and considered the behaviour of structured theory presentations under representation. That work was based on the simplifying assumption that logics are characterized as families of consequence relations on “closed” sentences. In this report we extend the notion of logical system to account for open formula, and study its basic properties. Following standard practice, we distinguish two types of logical system of open formulae that differ in the treatment of free variables, and show how they may be induced from a logical system of closed sentences. The technical notions of a logic presentation and a uniform encoding of a logical system in LF are generalized to the present setting.
Original languageEnglish
Title of host publicationCategory Theory and Computer Science
Subtitle of host publicationManchester, UK, September 5–8, 1989 Proceedings
EditorsDavid H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, Axel Poigné
PublisherSpringer
Pages250-272
Number of pages23
ISBN (Electronic)978-3-540-46740-3
ISBN (Print)978-3-540-51662-0
DOIs
Publication statusPublished - 1989

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
Volume389
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'Logic representation in LF'. Together they form a unique fingerprint.

Cite this