A New Type Theory for Representing Logics

Venue

Logic Programming and Automated Reasoning, 4^th International Conference, LPAR’93, St. Petersburg, Russia, July 13–20, 1993 Proceedings, pp. 146–157

Publication Year

1993

Identifiers

DOI: doi:10.1007/3-540-56944-8_49

Authors

Philippa Gardner

Abstract

We propose a new type theory for representing logics, called LF+ and based on the Edinburgh Logical Framework. The new framework allows us to give, apparently for the first time, general definitions which capture how well a logic has been represented. Using our definitions, we show that, for example, first-order logic can be wellrepresented in LF+, whereas linear and relevant logics cannot. These syntactic definitions of representation have a simple formulation as indexed isomorphisms, which both confirms that our approach is a natural one, and provides a link between type-theoretic and categorical approaches to frameworks.

Source Materials

Published Edition
BibTeX Citation