A Tableau Method for the Lambek Calculus based on a Matrix Characterization

AbstractWe propose a tableau method for the Lambek Calculus by adapting a method developed by Mantel and Otten for the multiplicative exponential fragment of the Linear Logic (MELL). We have incorporated new elements to the language of the tableau system and a new restriction to its closure conditions to deal with the noncommutative feature of the Lambek Calculus, considering a labelling technique developed for the matrix characterization method