Decidable Fragments of Calculi Used in CatLog

Studies in Computational Intelligence. 2021. Vol. 999. P. 1–24.

Kanovich M., Kuznetsov Stepan G., Kuznetsov S., Scedrov A.

CatLog is a categorial grammar parser/theorem-prover
developed by Glyn Morrill and his co-authors. CatLog is based on an
extension of Lambek calculus. A distinctive feature of this extension is
the usage of brackets for controlled non-associativity and a subexponential
modality whose contraction rule interacts with bracketing in a
sophisticated way. We consider two variants of the calculus, appearing in
different versions of CatLog. Both systems are, unfortunately, undecidable
in general.We consider fragments where the usage of subexponential
is restricted by so-called bracket non-negative/non-positive conditions,
prove that these fragments are decidable, and pinpoint their place in the
complexity hierarchy. We also consider a more complicated, but more
practically interesting problem of inducing (guessing) brackets. For this
problem, we prove one decidability and one undecidability result, and
leave some open questions for further research.

Keywords: Lambek calculus, исчисление Ламбека, Categorial grammars, Subexponential modalities, Bracket modalities, Категориальные грамматики, Субэкспоненциальные модальности, скобочные модальности

Publication based on the results of: Доказательства и модели (2021)