Session 6. Computational Logic

Substructural logics in type grammars: selected issues

Wojciech Buszkowski, Faculty of Mathematics and Computer Science, Adam Adam Mickiewicz Universityin Poznań, Poland , 
Substructural logics are nonclassical logics whose Gentzen-style sequent systems lack some/all structural rules, appearing in Gentzen systems for classical logic and intuitionistic logic: exchange, weakening, contraction, associativity. From the algebraic point of view, they are logics of residuation: implication(s) is (are) residual operation(s) for product (also called: fusion, multiplicative conjunction). The basic substructural logics are Full Lambek Calculus (FL), Full Nonassociative Lambek Calculus (FNL), their subsystems, e.g. Lambek Calculus (the multiplicative fragment of FL) and extensions with structural rules, new operations and additional axioms or rules. Many important nonclassical logics belong to this family, e.g. relevant logics, multi-valued and fuzzy logics, constructive logic with strong negation, linear logics, and in the limit also intuitionistic logic and classical logic.

Type grammars are formal grammars based on type-theoretic syntax and semantics. One assigns types to lexical atoms (words) of the language, and parsing procedures employ a type logic independent of the particular language. Type logics are certain substructural logics, most often basic logics from this class. The theory of type grammars shares some common ideas and goals with the Montagovian semantics of natural language but is mainly concerned with proof-theoretic and algebraic properties of type logics, used to describe many fine syntactic structures of natural languages and their semantic readings.

In this talk I'll present some selected results in this area, obtained in the last decade in Poznań (by myself and my collaborators). These are: (1) an interpolation lemma for finite theories based on FNL and its variants, (2) its applications in the proofs of strong finite model property and decidability, (3) interpretations of substructural logics in their subsystems, (4) results on the computational complexity of certain type logics and the generative capacity of type grammars.

Published in: CSLI Lecture Notes 168, Stanford, 2005, 77--93; LNCS 5533, 2009, 45--58; Journal of Logic and Computation 17.1, 2007, 199--217; Logic Journal of the IGPL 19.3, 2011, 437--454; Journal of Computer and System Sciences 78.6, 2012, 1899--1909; LNCS 8535, 2014, 30--43. Co-authors: Maciej Farulewski, Zhe Lin, Katarzyna Moroz.

Print version