Substructural Logics

Abstract

In this chapter we consider substructural implicational logics. These logics, as far as the implicational fragment is concerned, put some restrictions on the use of formulas in deductions. The restrictions may require either that every formula of the database must be used, or that it cannot be used more than once, or that it must be used according to a given ordering of database formulas. The denomination substructural logics can be explained by the fact that these systems restrict (some of) the structural rules of deduction, that is to say the contraction, weakening and permutation rules which are allowed both by classical and intuitionistic provability. Substructural logics have received an increasing interest in the computer science community because of their potential applications in a number of different areas, such as natural language processing, database update, logic programming, type-theoretic analysis by means of the so called Curry—Howard isomorphism and, more generally, the categorical interpretation of logics. We refer to [Došen, 1993; Ono, 1998; Ono, 1993; Routley et al., 1982] for a survey. Recently, Routley—Meyer semantics for substructural logics have been re-interpreted as modelling agent-interaction [Slaney and Meyer, 1997].