Full Lambek Calculus with Contraction is Undecidable

Number of the records: 1

1.

SYSNO ASEP	0442807
Document Type	J - Journal Article
R&D Document Type	Journal Article
Subsidiary J	Článek ve WOS
Title	Full Lambek Calculus with Contraction is Undecidable
Author(s)	Chvalovský, Karel (UIVT-O)_{SAI, RID, ORCID} Horčík, Rostislav (UIVT-O)_{SAI, RID}
Source Title	Journal of Symbolic Logic. - : Cambridge University Press - ISSN 0022-4812 Roč. 81, č. 2 (2016), s. 524-540
Number of pages	17 s.
Language	eng - English
Country	US - United States
Keywords	substructural logic ; full Lambek calculus ; contraction rule ; square-increasing residuated lattice ; equational theory ; decidability
Subject RIV	BA - General Mathematics
R&D Projects	GAP202/11/1632 GA ČR - Czech Science Foundation (CSF)
Institutional support	UIVT-O - RVO:67985807
UT WOS	000379947600008
EID SCOPUS	84977178290
DOI	10.1017/jsl.2015.18
Annotation	We prove that the set of formulae provable in the full Lambek calculus with the structural rule of contraction is undecidable. In fact, we show that the positive fragment of this logic is undecidable.
Workplace	Institute of Computer Science
Contact	Tereza Šírová, sirova@cs.cas.cz, Tel.: 266 053 800
Year of Publishing	2017

Number of the records: 1