Home  Online Resources  Table of Contents

Journal of Logic and Computation, Volume 8, Issue 6, pp. 809-838: Abstract.

A relevant analysis of natural deduction

SS Ishtiaq and DJ Pym

Department of Computer Science, Queen Mary & Westfield College, University of London, London E1 4NS, UK, E-mail: {si,pym}@dcs.qmw.ac.uk

We study a framework, RLF, for defining natural deduction presentations of linear and other relevant logics. RLF consists in a language together, in a manner similar to that of LF, with a representation mechanism. The language of RLF, the [lgr][Lgr][kgr]-calculus, is a system of first-order linear dependent function types which uses a function [kgr] to describe the degree of sharing of variables between functions and their arguments. The representation mechanism is judgements-as-types, developed for linear and other relevant logics. The [lgr][Lgr][kgr]-calculus is a conservative extension of the [lgr]II-calculus and RLF is a conservative extension of LF.

Keywords: Type theory, relevant logic, linear logic, natural deduction, logical frameworks.


[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 1998.