A tableau method for the Lambek calculus based on a matrix characterization

DOI10.1016/S1571-0661(04)80855-7MaRDI QIDQ4924540zbMATH OpenOpenAlexFDO

Authors Leonardo Bruno Vana, Marcelo da S. Corrêa

Publication date 6 June 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s1571-0661(04)80855-7

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47)

Recommendations

• Using tableaux to automate the Lambek and other categorial calculi
• On Lambek's restriction in the presence of exponential modalities
• Lambek's syntactic calculus and noncommutative variants of linear logic: laws and proof-nets
• Reconciling Lambek's restriction, cut-elimination and substitution in the presence of exponential modalities
• Lambek Calculus in Natural Deduction

Cites work

• A comparison between lambek syntactic calculus and intuitionistic linear propositional logic
• scientific article; zbMATH DE number 1301753 (Why is no real title available?)
• scientific article; zbMATH DE number 1341478 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• Logic Programming with Focusing Proofs in Linear Logic
• On Matrices with Connections
• On proof normalization in linear logic
• T-string unification: unifying prefixes in non-classical proof methods
• The Mathematics of Sentence Structure

Cited in

(1)

• Using tableaux to automate the Lambek and other categorial calculi

Describes a project that uses

Uses Software

• linTAP

This page was built for publication: A tableau method for the Lambek calculus based on a matrix characterization

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4924540)