Linear Logic

Linear logic and other substructural logics have been a subject of considerable academic interest. One of the earlier substructural logics is the Lambek Calculus, developed for representing sentences in natural languages. Relevance Logic rejects weakening with the intuition that all premises of a sequent must be relevant to entail the consequence relation. Linear logic has served as a basis for several mechanisations, and there is wide current research in the use of these mechanisations as possible tools for verification. We have already implemented Linear Logic in the Isabelle theorem prover.

The notion that some valid formulae are consumed in the proof process and are therefore transient suggests that some substructural logics may be natural formalisms for expressing dynamic properties, which require the invalidation of old properties and the validation of new properties over the computation. In fact, they have already been proposed and used as a metalanguage to describe models of computation, with varying degrees of success. A first step in exploring this approach is to study several varieties of substructural logics in a uniform framework, guided by case studies of interest to formal methodologists. This line of work is currently examining varieties of substructural logics vis-a-vis verification tasks, in a pragmatic way and using theorem provers.

Staff involved: Sara Kalvala