% lcr.bbl % Mati Pentus, 2006/12/04, 2011/08/20 % cp1251 \newcommand{\df}{\protect\nolinebreak\hspace{0pt}\mbox{-}\protect \nolinebreak\hspace{0pt}} \begin{thebibliography}{999} \bibitem{Bus1993} Бушковский~В\@. Синтаксическое исчисление Ламбека и его семантика // Логические исследования. Вып.~1.~--- М.:~Наука, 1993.~--- С.~77---96. \bibitem{Gla1966} Гладкий~А.~В\@. Лекции по математической лингвистике для студентов НГУ.~--- Новосибирск.: Издательство~НГУ, 1966. \bibitem{Gla1973} Гладкий~А.~В\@. Формальные грамматики и языки.~--- М.: Наука, 1973. \bibitem{GM1969} Гладкий~А.~В., Мельчук~И.~А\@. Элементы математической лингвистики.~--- М.: Наука, 1969.~--- 192~с.:~ил. \bibitem{Gri1983} Гришин~В.~Н\@. Об одном обобщении системы Айдукевича---Ламбека // Исследования по неклассическим логикам и формальным системам.~--- М.:~Наука, 1983.~--- С.~315---334. %% not 315---343 \bibitem{Kuznetsov2009Vestnik} Кузнецов~С.~Л\@. Об исчислении Ламбека с одним делением и одним примитивным типом, допускающем пустые антецеденты // Вестник Московского университета. Серия~1, Математика. Механика.~--- 2009.~--- \No~2.~--- С.~\mbox{62---65}. % %Доказывается следующее утверждение: правило вывода, заданное схемой, допустимо в исчислении Ламбека с одним делением $\mathrm{L}^*(\backslash)$, допускающем пустые антецеденты, тогда и только тогда, когда оно допустимо во фрагменте $\mathrm{L}^*(\backslash)$ с одним примитивным типом $\mathrm{L}^*(\backslash; p_1)$. %Для этого применяется подстановка типов, сводящая выводимость в $\mathrm{L}^*(\backslash)$ к выводимости в $\mathrm{L}^*(\backslash;p_1)$. \bibitem{Kuznetsov2009dipl} Кузнецов~С.~Л\@. О~грамматиках, основанных на двух вариантах исчисления Ламбека: Дипломная работа / Кафедра математической логики и теории алгоритмов МГУ.~--- М., 2009.~--- 12~с. % %В работе доказывается, что класс $\mathrm{L}(\li;p_1)$-языков совпадает %с классом контекстно-свободных языков без пустого слова, а классы %$\mathrm{L}^*$-языков и $\mathrm{L}_1$-языков совпадают с классом всех контекстно-свободных языков. %Вводится исчисление $\mathrm{MCLL}'$, консервативное над~$\mathrm{L}$. %Вводится понятие сильной сети доказательства, дающее критерий для выводимости в $\mathrm{MCLL}'$. \bibitem{Kuznetsov2011Vestnik} Кузнецов~С.~Л\@. Об исчислении Ламбека с единицей и одним делением // Вестник Московского университета. Серия~1, Математика. Механика.~--- 2011.~--- \No~4.~--- С.~\mbox{58---61}. % %В статье предъявляется подстановка, сводящая выводимость в исчислении Ламбека с единицей с одним делением к выводимости в исчислении Ламбека с одним делением, допускающем пустые антецеденты. %При помощи этой подстановки устанавливается существование алгоритма, за полиномиальное время проверяющего выводимость в исчислении Ламбека с единицей с одним делением. \bibitem{Minina1999} Минина~В.~А\@. Необходимое условие эквивалентности формул некоммутативной линейной логики: Курсовая работа / Кафедра математической логики и теории алгоритмов МГУ.~--- М., 1999.~--- 7~с. \bibitem{Minina2001} Минина~В.~А\@. Полнота синтаксического исчисления Ламбека с операцией инволюции: Дипломная работа / Кафедра математической логики и теории алгоритмов МГУ.~--- М., 2001.~--- ???~с. % %Доказана R-полнота исчисление Ламбека с инволюцией. \bibitem{Pentus2004} Пентус~А.~Е., Пентус~М.~Р\@. Теория формальных языков: Учебное пособие.~--- М.: \mbox{Изд-во} ЦПИ при механико\df математическом \mbox{ф-те} МГУ, 2004.~--- 80~с. \bibitem{Pentus2006MTFYa} Пентус~А.~Е., Пентус~М.~Р\@. Математическая теория формальных языков: Учебное пособие.~--- М.:~Интернет-университет информационных технологий; БИНОМ. Лаборатория знаний, 2006.~--- 247~с.:~ил.~--- (Серия "Основы информатики и математики"). \bibitem{Pentus2006FPM} Пентус~А.~Е., Пентус~М.~Р\@. Атомарная теория деления двусторонних идеалов полуколец // Фундаментальная и прикладная математика.~--- 2006.~--- Т.~12, \No~2.~--- С.~\mbox{201---208}. \bibitem{Pentus1995FPM} Пентус~М.~Р\@. Исчисление Ламбека и формальные грамматики // Фундаментальная и прикладная математика.~--- 1995.~--- Т.~1, \No~3.~--- С.~\mbox{729---751}. \bibitem{Pentus1996kd} Пентус~М.~Р\@. Исчисление Ламбека и формальные грамматики: Дис.~\ldots канд.\ физ.-мат.\ наук: 01.01.06.~--- Защищена 01.03.1996; Утв.~14.06.1996; 01910048811.~--- М., 1996.~--- 69~с.~--- Библиогр.: с.~\mbox{67---69}. \bibitem{Pentus1997YSTM} Пентус~М.~Р\@. Синтаксическое исчисление Ламбека и формальные грамматики // YSTM'96: ``Молодежь и наука~--- третье тысячелетие''. Труды международного конгресса.\ Т.~1 / Под ред.\ %И.~Б.~Федорова, К.~С.~Колесникова, А.~О.~Карпова.~--- И.~Б.~Федорова и~др.~--- М.: НТА ``Актуальные проблемы фундаментальных наук'', 1997.~--- С.~\mbox{I-15---I-16}. \bibitem{Pentus1999FPM} Пентус~М.~Р\@. Полнота синтаксического исчисления Ламбека // Фундаментальная и прикладная математика.~--- 1999.~--- Т.~5, \No~1.~--- С.~\mbox{193---219}. \bibitem{Pentus2000FPM} Пентус~М.~Р\@. Атомарные теории семейств полугрупп с~делением // Фундаментальная и прикладная математика.~--- 2000.~--- Т.~6, \No~2.~--- С.~\mbox{627---632}. \bibitem{Pentus2000dd} Пентус~М.~Р\@. Полнота исчисления Ламбека: Дис.~\ldots доктора физ.-мат.\ наук: 01.01.06.~--- Защищена 06.10.2000; Утв.~12.01.2001; 01960004678.~--- М., 2000.~--- 165~с.~--- Библиогр.: с.~\mbox{158---165}. \bibitem{Savateev2009diss} Саватеев~Ю.~В\@. Алгоритмическая сложность фрагментов исчисления Ламбека : дис.\ \ldots канд.\ физ.-мат.\ наук : 01.01.06 : защищена 11.12.2009.~--- М., 2009.~--- 75~с. \bibitem{Savateev2009Vestnik} Саватеев~Ю.~В\@. Распознавание выводимости для исчисления Ламбека с одним делением // Вестник Московского университета. Серия~1, Математика. Механика.~--- 2009.~--- \No~2.~--- С.~\mbox{59---62}. % %В работе описывается полиномиальный алгоритм для определения выводимости в исчислении Ламбека с одним делением. \bibitem{Safiullin2007} Сафиуллин~А.~Н\@. Выводимость допустимых правил с~простыми посылками в~исчислении Ламбека // Вестник Московского университета. Серия~1, Математика. Механика.~--- 2007.~--- \No~4.~--- С.~\mbox{72---76}. \bibitem{Sorokin2011Vestnik} Сорокин~А.~А\@. О длине совмещающего типа в исчислении Ламбека // Вестник Московского университета. Серия~1, Математика. Механика.~--- 2011.~--- \No~3.~--- С.~\mbox{10---14}. % %В 1992 году г. М. Р. Пентусом был установлен критерий существования такого типа $C$, что для данных типов $A$ и $B$ секвенции $A \to C$ и $B \to C$ являются выводимыми в исчислении Ламбека. %В данной статье предлагается алгоритм построения типа $C$ (в случае, если он существует) и доказывается квадратичная верхняя оценка на его длину. \bibitem{Tur1995} Турмухамбетова~Г.~А\@. О~полиномиальной разрешимости в~некоммутативной линейной логике: Дипломная работа / Кафедра математической логики и теории алгоритмов МГУ.~--- М., 1995.~--- 14~с. \bibitem{Kharitonov2007} Харитонов~А.~В\@. Полнота исчисления Ламбека относительно моделей на конечных полугруппах с~делением: Курсовая работа / Кафедра математической логики и теории алгоритмов МГУ.~--- М., 2007.~--- 7~с. \bigbreak \bibitem{AD1993} Allwein~G., Dunn~J.~M\@. Kripke models for linear logic // Journal of Symbolic Logic.~--- 1993.~--- Vol.~58, \No~2.~--- P.~\mbox{514---545}. \bibitem{AM1994} Andr\'eka~H., Mikul\'as~Sz\@. Lambek calculus and its relational semantics // Journal of Logic, Language and Information.~--- 1994.~--- Vol.~3, \No~1.~--- P.~1---37. % % The theory of representable lower semilattice-ordered residuated semigroups is finitely axiomatizable. % A representable lower semilattice-ordered residuated semigroup has the intersection, product, and two division operators. % Arnon Avron \bibitem{Avr1988} Avron~A\@. The semantics and proof theory of linear logic // Theoretical Computer Science.~--- 1988.~--- Vol.~57, \No~2/3.~--- P.~\mbox{161---184}. \bibitem{Bar1953} Bar-Hillel Y\@. A quasi-arithmetical notation for syntactic description // Langugage.~--- 1953.~--- Vol.~29.~--- P.~47---58. \bibitem{BGS1960} Bar-Hillel Y., Gaifman C., Shamir E\@. On categorial and phrase-structure grammars // Bull.\ Res.\ Council Israel Sect.~F.~--- 1960.~--- Vol.~9F.~--- P.~1---16. \bibitem{Bul} Buli\'nska~M\@. On the Complexity of Nonassociative Lambek Calculus with Unit // Studia Logica.~--- 2009.~--- Vol.~93, \No~1.~--- P.~1---14. \bibitem{Bus1978} Buszkowski~W\@. Undecidability of some logical extensions of Ajdukiewicz--Lambek calculus // Studia Logica.~--- 1978.~--- Vol.~37.~--- P.~59---64. \bibitem{Bus1982C} Buszkowski~W\@. Compatibility of categorial grammar with an associated category system // Zeitschrift f\"{u}r mathematische Logik und Grundlagen der Mathematik.~--- 1982.~--- Vol.~28.~--- P.~229---238. \bibitem{Bus1982S} Buszkowski~W\@. Some decision problems in the theory of syntactic categories // Zeitschrift f\"{u}r mathematische Logik und Grundlagen der Mathematik.~--- 1982.~--- Vol.~28.~--- P.~539---548. \bibitem{Bus1985A} Buszkowski~W\@. Algebraic models of categorial grammars // Proceedings of the 7th International Congress of Logic, Methodology, and Philosophy of Science.~--- New York: Plenum Press, 1985.~--- P.~403---426. \bibitem{Bus1985E} Buszkowski W\@. The equivalence of unidirectional Lambek categorial grammars and context-free grammars // Zeitschrift f\"{u}r mathematische Logik und Grundlagen der Mathematik.~--- 1985.~--- Vol.~31.~--- P.~369---384. \bibitem{Bus1986C} Buszkowski~W\@. Completeness Results for Lambek Syntactic Calculus // Zeitschrift f\"{u}r mathematische Logik und Grundlagen der Mathematik.~--- 1986.~--- Vol.~32.~--- P.~13---28. \bibitem{Bus1991G} Buszkowski~W\@. On generative capacity of the Lambek calculus // Logics in AI: European Workshop JELIA '90. Amsterdam, The Netherlands, September 1990. Proceedings / Editor J.~van~Eijck.~--- Berlin: Springer-Verlag, 1991.~--- P.~139---152.~--- (Lecture Notes in Computer Science; vol.~478. Lecture Notes in Artificial Intelligence). \bibitem{Bus1993E} Buszkowski~W\@. On the Equivalence of Lambek Categorial Grammars and Basic Categorial Grammars.~--- Amsterdam: Institute for Logic, Language and Computation, University of Amsterdam, 1993.~--- 21~p.~--- (ILLC Prepublication Series; \mbox{LP---93---07}). \bibitem{Bus1996} Buszkowski~W\@. The finite model property for BCI and related systems // Studia Logica.~--- 1996.~--- Vol.~57.~--- P.~303---323. % %We prove the finite model property (fmp) for BCI and BCI with additive conjunction, which answers some open questions in Meyer and Ono. %We also obtain similar results for some restricted versions of these systems in the style of the Lambek calculus. %The key tool is the method of barriers which was earlier introduced by the author to prove fmp for the product-free Lambek calculus and the commutative product-free Lambek calculus. \bibitem{Bus2003} Buszkowski~W\@. Type logics in grammar // Trends in Logic: 50 Years of Studia Logica / Editors V.~F.~Hendricks, J.~Malinowski.~--- Kluwer Academic Publishers, 2003.~--- P.~337---382.~--- (Trends in Logic; vol.~21). \bibitem{Car1997} Carpenter~B\@. Type-Logical Semantics.~--- Cambridge~etc.: The MIT Press, 1997.~--- XXI,~575~p.~--- (Language, Speech, and Communication). \bibitem{OBW1988} Categorial Grammars and Natural Language Structures / Editors R.~T.~Oehrle, E.~Bach, D.~Wheeler.~--- Dordrecht: Reidel, 1988. \bibitem{Coh1967} Cohen J. M\@. The equivalence of two concepts of categorial grammar // Information and Control.~--- 1967.~--- Vol.~10.~--- P.~475---484. \bibitem{Dos1985} Do\v{s}en~K\@. A Completeness Theorem for the Lambek Calculus of Syntactic Categories // Zeitschrift f\"{u}r mathematische Logik und Grundlagen der Mathematik.~--- 1985.~--- Vol.~31.~--- P.~235---241. \bibitem{Dos1988} Do\v{s}en~K\@. Sequent systems and groupoid models // Studia Logica.~--- 1988.~--- Vol.~47, \No~4.~--- P.~353---385; 1989.~--- Vol.~48, \No~1.~--- P.~41---65.~--- Addenda and corrigenda: 1990.~--- Vol.~49.~--- P.~614. \bibitem{Dos1992} Do\v{s}en~K\@. A brief survey of frames for the Lambek calculus // Zeitschrift f\"{u}r mathematische Logik und Grundlagen der Mathematik.~--- 1992.~--- Vol.~38, \No~2.~--- P.~179---187. \bibitem{Fuc1963} Fuchs~L\@. Partially Ordered Algebraic Systems.~--- Oxford: Pergamon Press, 1963.~--- Русский перевод: Фукс~Л\@. Частично упорядоченные алгебраические системы /~Пер.\ с~англ.\ И.~В.~Стеллецкого.~--- М.: Мир, 1965.~--- 342~с. \bibitem{GO2008} Galatos~N., Ono~H\@. Cut elimination and strong separation for substructural logics: an algebraic approach [Preprint].~--- Denver: University of Denver, Department of Mathematics, 2008.~--- 56 p.~--- (M08/26).~--- URL: \url{http://www.math.du.edu/data/preprints/m0826.pdf} (дата обращения: 31.01.2009). \bibitem{GO2010} Galatos~N., Ono~H\@. Cut elimination and strong separation for substructural logics: an algebraic approach // Annals of Pure and Applied Logic.~--- 2010.~--- Vol.~161, \No~9.~--- P.~\mbox{1097---1133}. % http://web.cs.du.edu/~ngalatos/research/slalgebra081020.pdf % % We develop a general algebraic and proof-theoretic study of substructural logics that may lack associativity, along with other structural rules. % $\mathrm{L}^*$ is complete with respect to finite residuated semigroups. \bibitem{Gin1966} Ginsburg~S\@. The Mathematical Theory of Context-free Languages.~--- New York: McGraw---Hill, 1966.~--- Русский перевод: Гинзбург~С\@. Математическая теория контекстно\df свободных языков /~Пер.\ с~англ.\ А.~Я.~Диковского, Л.~С.~Модиной.~--- М.: Мир, 1970.~--- 326~с. \bibitem{Gir1987} Girard~J.-Y\@. Linear logic // Theoretical Computer Science.~--- 1987.~--- Vol.~50, \No~1.~--- P.~\mbox{1---102}. \bibitem{Hen1993} Hendriks~H\@. Studied Flexibility. Categories and Types in Syntax and Semantics: Ph.D.~thesis.~--- Amsterdam, 1993.~--- (ILLC Dissertation series; \mbox{1993---5}). \bibitem{HH1986} Hoare~C.~A.~R., He~J\@. The weakest prespecification // Fund.\ Inform.~--- 1986.~--- Vol.~9, \No~1.~--- P.~51---84; 1986.~--- Vol.~9, \No~2.~--- P.~217---251. \bibitem{JO2009} Je\.{z}~A., Okhotin~A\@. One-nonterminal conjunctive grammars over a unary alphabet // Computer Science --- Theory and Applications / Editors E.A. Hirsch et al..~--- Berlin: Springer, 2009.~--- P.~191---202.~--- (Lecture Notes in Computer Science; vol.~5675). % http://www.ii.uni.wroc.pl/~aje/prace/CSR2009.pdf % % The compressed membership problem for one-nonterminal conjunctive grammars over {a} is proved to be EXPTIME-complete. % The equivalence, finiteness and emptiness problems for these grammars are shown to be undecidable. \bibitem{Kana1992} Kanazawa~M\@. The Lambek calculus enriched with additional connectives // Journal of Logic, Language and Information.~--- 1992.~--- Vol.~1.~--- P.~141---171. \bibitem{Kano1992LICS} Kanovich~M.~I\@. Horn programming in linear logic is NP-complete // Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science: June 22---25, 1992. Santa Cruz, California, USA.~--- Los Alamitos, California: IEEE Computer Society Press, 1992.~--- P.~\mbox{200---210}. \bibitem{Kuznetsov2009EnVestnik} Kuznetsov~S.~L\@. Lambek calculus with one division and one primitive type permitting empty antecedents // Moscow University Mathematics Bulletin.~--- 2009.~--- Vol.~64, \No~2.~--- P.~\mbox{76---79}. % %Translation of \cite{Kuznetsov2009Vestnik} % %The following assertion is proved: an inference rule given by a scheme is admissible in the Lambek calculus with one division $\mathrm{L}^*(\backslash)$ permitting empty antecedents if and only if it is admissible in the fragment of $\mathrm{L}^*(\backslash)$ with one primitive type $\mathrm{L}^*(\backslash;p_1)$. %To do that, a type substitution is used which reduces the derivability in $\mathrm{L}^*(\backslash)$ to the derivability in $\mathrm{L}^*(\backslash;p_1)$. \bibitem{Lal1979} Lallement~G\@. Semigroups and Combinatorial Applications.~--- New York~etc.: John Wiley \& Sons, 1979.~--- Русский перевод: Лаллеман~Ж\@. Полугруппы и комбинаторные приложения /~Пер.\ с~англ.\ И.~О.~Корякова.~--- М.: Мир, 1985.~--- 440~с.:~ил. \bibitem{Lam1958} Lambek~J\@. The mathematics of sentence structure // American Mathematical Monthly.~--- 1958.~--- Vol.~65, \No~3.~--- P.~154---170.~--- Русский перевод: Ламбек~И\@. Математическое исследование структуры предложений // Математическая лингвистика: Сборник переводов / Под ред.\ Ю.~А.~Шрейдера и~др.~--- М.: Мир, 1964.~--- С.~47---68. \bibitem{Lam1961} Lambek~J\@. On the calculus of syntactic types // Structure of Language and Its Mathematical Aspects / Editor R.~Jakobson.~--- Providence, RI: Amer.\ Math.\ Soc., 1961.~--- (Proc.\ Symposia Appl.\ Math.; vol.~12).~--- P.~166---178. \bibitem{Lam1966} Lambek J\@. Lectures on Rings and Modules.~--- Waltham, Massachusetts, etc.: Blaisdell, 1966.~--- Русский перевод: Ламбек~И\@. Кольца и модули /~Пер.\ с~англ.\ А.~В.~Михалёва.~--- М.: Мир, 1971.~--- 280~с. \bibitem{Lam1968} Lambek~J\@. Deductive systems and categories~I. Syntactic calculus and residuated categories // Math.\ Systems Theory.~--- 1968.~--- Vol.~2, \No~4.~--- P.~\mbox{287---318}. %% ?not 278---318 \bibitem{Lam1969} Lambek~J\@. Deductive systems and categories~II. Standard constructions and closed categories // Category Theory, Homology Theory and Their Applications~I: Proceedings of the Conference held at the Seattle Research Center of the Battelle Memorial Institute, June 24--July 19, 1968 / Editor P.~Hilton.~--- Berlin: Springer, 1969.~--- P.~76---122.~--- (Springer Lecture Notes in Mathematics; vol.~86). \bibitem{Lam1972} Lambek~J\@. Deductive systems and categories~III. Cartesian closed categories, intuitionist propositional calculus, and combinatory logic // Toposes, Algebraic Geometry, and Logic: Proceedings of the Conference held at the Dalhousie University, Halifax, Nova Scotia, January 16--19, 1971 / Editor F.~Lawvere.~--- ?Berlin: ?Springer, 1972.~--- P.~57---82.~--- (Springer Lecture Notes in Mathematics; vol.~274). %% ISBN 3-540-05920-2 \bibitem{Lam1993F} Lambek~J\@. From categorial grammar to bilinear logic // Substructural Logics / Editors K.~Do\v{s}en, P.~Schroeder-Heister.~--- Oxford: Clarendon Press, 1993.~--- P.~207---237.~--- (Studies in Logic and Computation; vol.~2). \bibitem{Lec1992} Lecomte~A\@. Proof-nets and dependencies // Proceedings of COLING 1992, 14th International Conference on Computational Linguistics, August 23--28, 1992, Nantes, France.~--- 1992.~--- P.~394---400. \bibitem{Lec1993} Lecomte~A\@. Towards efficient parsing with proof-nets // EACL 1993, 6th Conference of the European Chapter of the Association for Computational Linguistics, April 21-23, 1993.~--- Utrecht: OTS~--- Research Institute for Language and Speech, Utrecht University, 1993.~--- P.~269---276. % Wendy MacCaull \bibitem{MCau1997} MacCaull~W\@. Relational proof systems for linear and other substructural logics // Logic Journal of the IGPL.~--- 1997.~--- Vol.~5, \No~5?.~--- P.~\mbox{673---697}. \bibitem{MCau1998} MacCaull~W\@. Realtional semantics and a~relational proof system for full Lambek calculus // Journal of Symbolic Logic.~--- 1998.~--- Vol.~63, \No~2.~--- P.~\mbox{623---637}. % Ewa Orlowska \bibitem{MCO2002} MacCaull~W., Orlowska~E\@. Correspondence results for relational proof systems with application to the Lambek calculus // Studia Logica.~--- 2002.~--- Vol.~71, \No~3.~--- P.~\mbox{389---414}. \bibitem{Mar1967} Marcus~S\@. Algebraic Linguistics: Analytical Models.~--- New York, London: Academic Press, 1967.~--- (Mathematics in Science and Engineering; vol.~29).~--- Русский перевод: Маркус~С\@. Теоретико-множественные модели языков /~Пер.\ с~англ.\ М.~В.~Арапова.~--- М.: Наука, 1970.~--- 332~с. \bibitem{Met1999} M\'etayer~F\@. Polynomial equivalence among systems $\mathrm{LLNC}$, $\mathrm{LLNC}_a$ and $\mathrm{LLNC}_0$. // Theoretical Computer Science.~--- 1999.~--- Vol.~227, No~1.~--- P.~221--229.~--- URL: \url{http://www.pps.jussieu.fr/~metayer/PDF/poleq.pdf} (дата обращения: 28.03.2011). \bibitem{Mik1992} Mikul\'as~Sz\@. The Completeness of the Lambek Calculus with respect to Relational Semantics.~--- Amsterdam: Institute for Logic, Language and Computation, University of Amsterdam, 1992.~--- 21~p.~--- (ILLC Prepublication Series; \mbox{LP---92---03}). \bibitem{Mik1995} Mikul\'as~Sz\@. Taming Logics: Ph.D.~thesis.~--- Amsterdam, 1995.~--- 123~p.~--- (ILLC Dissertation Series; \mbox{1995-12}). \bibitem{Mik2010} Mikul\'as~Sz\@. On representable ordered residuated semigroups.~--- To appear in Logic Journal of the IGPL. % Preliminary version: http://www.dcs.bbk.ac.uk/~szabolcs/Mik-IGPL-fin.pdf % % A representable relation algebra has Booleans, the diagonal, product, and converse (the division operators are definable). % The equational theory of representable lattice-ordered residuated semigroups is not finitely axiomatizable. % Moreover, the equational and quasiequational theories of R-models with union, intersection, product, and two division operators is not finitely axiomatizable. % Michael Moortgat % Михаэл Мортгат \bibitem{Moo1988} Moortgat~M\@. Categorial Investigations. Logical and Linguistic Aspects of the Lambek Calculus: Ph.D.~thesis.~--- Dordrecht: Foris, 1988.~--- XVII,~270~p. \bibitem{Ono1993} Ono~H\@. Semantics for substructural logics // Substructural Logics / Editors K.~Do\v{s}en, P.~Schroeder-Heister.~--- Oxford: Clarendon Press, 1993.~--- P.~259---291.~--- (Studies in Logic and Computation; vol.~2). \bibitem{Orl1988} Orlowska~E\@. Relational interpretation of modal logics // Polish Acad.\ Sci.\ Inst.\ Philos.\ Sociol.\ Bull.\ Sect.\ Logic.~--- 1988.~--- Vol.~17, \No~1.~--- P.~\mbox{2---14}. \bibitem{Pan1994} Pankratiev~N\@. On the completeness of the Lambek calculus with respect to relativized relational semantics // Journal of Logic, Language and Information.~--- 1994.~--- Vol.~3, \No~3.~--- P.~233---246. \bibitem{Pentus1992LCS02} Pentus~M\@. Equivalent types in Lambek calculus and linear logic.~--- Серия Математическая логика и теоретическая информатика, \No~2: [Препринт] / РАН, Математический институт им.~В.~А.~Стеклова, отдел математической логики.~--- М.,~1992.~--- 21~с. URL: \url{http://lpcs.math.msu.su/~pentus/ftp/papers/lcs2.pdf} (дата обращения: 20.11.2010). \bibitem{Pentus1992LCS08} Pentus~M\@. Lambek grammars are context free.~--- Серия Математическая логика и теоретическая информатика, \No~8: [Препринт] / РАН, Математический институт им.~В.~А.~Стеклова, отдел математической логики.~--- М.,~1992.~--- 10~с. \bibitem{Pentus1993ILLC14} Pentus~M\@. Lambek calculus is L-complete.~--- ILLC Prepublication Series, \mbox{LP-93-14}.~--- Amsterdam: Institute for Logic, Language and Computation, University of Amsterdam, 1993.~--- 36~p. \bibitem{Pentus1993LICS} Pentus~M\@. Lambek grammars are context free // Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science: June 19---23, 1993. Montreal, Canada.~--- Los Alamitos, California: IEEE Computer Society Press, 1993.~--- P.~\mbox{429---433}. \bibitem{Pentus1993ILLC03} Pentus~M\@. The conjoinability relation in Lambek calculus and linear logic.~--- ILLC Prepublication Series, \mbox{ML-93-03}.~--- Amsterdam: Institute for Logic, Language and Computation, University of Amsterdam, 1993.~--- 20~p. \bibitem{Pentus1994LICS} Pentus~M\@. Language completeness of the Lambek calculus // Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science: July 4---7, 1994. Paris, France.~--- Los Alamitos, California: IEEE Computer Society Press, 1994.~--- P.~\mbox{487---496}. \bibitem{Pentus1994JLLI} Pentus~M\@. The conjoinability relation in Lambek calculus and linear logic // Journal of Logic, Language and Information.~--- 1994.~--- Vol.~3, \No~2.~--- P.~\mbox{121---140}. \bibitem{Pentus1995APAL} Pentus~M\@. Models for the Lambek calculus // Annals of Pure and Applied Logic.~--- 1995.~--- Vol.~75, \No~1---2.~--- P.~\mbox{179---213}. \bibitem{Pentus1997JSL} Pentus~M\@. Product-free Lambek calculus and context-free grammars // Journal of Symbolic Logic.~--- 1997.~--- Vol.~62, \No~2.~--- P.~\mbox{648---660}. \bibitem{Pentus1998FMC} Pentus~M\@. Free monoid completeness of the Lambek calculus allowing empty premises // Logic Colloquium '96: Proceedings of the colloquium held in San Sebastian, Spain, July 9---15, 1996 / Editors J.~M.~Larrazabal, D.~Lascar, G.~Mints.~--- Berlin: Springer, 1998.~--- P.~\mbox{171---209}.~--- (Lecture Notes in Logic; vol.~12). \bibitem{Pentus1998LCFL} Pentus~M\@. Lambek calculus and formal languages // Logic Colloquium '95: Proceedings of the Annual European Summer Meeting of the Association of Symbolic Logic, held in Haifa, Israel, August \mbox{9---18}, 1995 / Editors J.~A.~Makowsky, E.~V.~Ravve.~--- Berlin: Springer, 1998.~--- P.~\mbox{269---272}.~--- (Lecture Notes in Logic; vol.~11). \bibitem{Pentus1999PCG} Pentus~M\@. Lambek calculus and formal grammars // Provability, Complexity, Grammars / L.~D.~Beklemishev, M.~Pentus, N.~K.~Vereshchagin.~--- American Mathematical Society, 1999.~--- \penalty-8000 P.~\mbox{57---86}.~--- (American Mathematical Society Translations. \penalty-8000 Series 2; vol.~192). \bibitem{Pentus2003CUNY} Pentus~M\@. Lambek calculus is $ \mathrm{NP} $-complete [Электронный ресурс].~--- Technical Report \mbox{TR-2003005} / CUNY Ph.D.~Program in Computer Science.~--- New York: CUNY Graduate Center, 2003.~--- 20~p.~--- URL: \url{http://www.cs.gc.cuny.edu/tr/techreport.php?id=79} (дата обращения: 29.11.2006). \bibitem{Pentus2005CSLI} Pentus~M\@. Characterization of atomicity in Lambek calculus and bilinear logic // Language and Grammar: Studies in Mathematical Linguistics and Natural Language / Editors C.~Casadio, P.~J.~Scott, R.~A.~G.~Seely.~--- CSLI Publications, 2005.~--- P.~\mbox{55---76}.~--- (CSLI Lecture Notes; vol.~160). \bibitem{Pentus2006TCS} Pentus~M\@. Lambek calculus is $ \mathrm{NP} $-complete // Theoretical Computer Science.~--- 2006.~--- Vol.~357, \No~1/3.~--- P.~\mbox{186---201}. \bibitem{Pentus2010LA} Pentus~M\@. A~Polynomial-Time Algorithm for Lambek Grammars of Bounded Order // Linguistic Analysis.~--- 2010.~--- Vol.~36, \No~1---4.~--- P.~\mbox{441---471}. % %We present a deterministic algorithm for solving the derivability problem for the Lambek calculus (the syntactic calculus with left division, right division, and multiplication, introduced by J.~Lambek in 1958) and a similar algorithm for the Lambek calculus allowing empty premises. %These algorithms work in time polynomial in the input length if the order of all syntactic types is bounded by a constant (it is known that for unbounded order the derivability problem is NP-complete). %The algorithms are based on a method for deciding derivability in the multiplicative fragment of the cyclic linear logic. %This method also yields an algorithm for solving the membership problem in Lambek grammars, which works in time polynomial in the grammar size and string length provided the order of all syntactic types is bounded by a constant. \bibitem{Pentus2010AiML} Pentus~M\@. Complexity of the Lambek Calculus and Its Fragments // Advances in Modal Logic, Volume~8 / Editors L. Beklemishev, V. Goranko and V. Shehtman.~--- College Publications, 2010.~--- P.~\mbox{310---329}.~-- URL: \url{http://aiml.net/volumes/volume8/Pentus.pdf} (дата обращения: 18.11.2010). % Dirk Roorda % Дирк Рорда \bibitem{Roo1991} Roorda~D\@. Resource Logics: Proof-theoretical Investigations: Ph.D.~thesis.~--- Amsterdam, 1991.~--- 138~p. \bibitem{Roo1994} Roorda D\@. Interpolation in fragments of classical linear logic // Journal of Symbolic Logic.~--- 1994.~--- Vol.~59, \No~2.~--- P.~419---444. \bibitem{Savateev2006Utrecht} Savateev~Y\@. The derivability problem for Lambek calculus with one division [Электронный ресурс].~--- Preprint \mbox{56} / Artificial Intelligence Preprint Series.~--- Utrecht University, 2006.~--- 8~p.~--- URL: \url{http://www.phil.uu.nl/preprints/ckipreprints/PREPRINTS/preprint056.pdf} (дата обращения: 13.12.2006). % %In this paper we prove that the derivability problem for Lambek calculus with one division is decidable in polynomial time and present an algorithm for it. \bibitem{Savateev2008CSR} Savateev~Y\@. Lambek grammars with one division are decidable in polynomial time // Computer Science --- Theory and Applications / Editors E.A. Hirsch et al..~--- Berlin: Springer, 2008.~--- P.~273---282.~--- (Lecture Notes in Computer Science; vol.~5010). % %Lambek grammars provide a useful tool for studying formal and natural languages. %The generative power of unidirectional Lambek grammars equals that of context-free grammars. %However, no feasible algorithm was known for deciding membership in the corresponding formal languages. %In this paper we present a polynomial algorithm for deciding whether a given word belongs to a language generated by a given unidirectional Lambek grammar. \bibitem{Savateev2008CUNY} Savateev~Y\@. Product-free Lambek Calculus is $ \mathrm{NP} $-complete [Электронный ресурс].~--- Technical Report \mbox{TR-2008012} / CUNY Ph.D.~Program in Computer Science.~--- New York: CUNY Graduate Center, 2008.~--- 15~p.~--- URL: \url{http://www.cs.gc.cuny.edu/tr/techreport.php?id=363} (дата обращения: 08.04.2009). % %In this paper we prove that the derivability problems for product-free Lambek calculus and product-free Lambek calculus allowing empty premises are NP-complete. %Also we introduce a new derivability characterization for these calculi. \bibitem{Savateev2009LFCS} Savateev~Y\@. Product-free Lambek calculus is NP-complete // Logical Foundations of Computer Science, International Symposium, LFCS 2009, Deerfield Beach, FL, USA, January 3---6, 2009. Proceedings / Editors S.~N.~Artemov and A.~Nerode.~--- Berlin: Springer, 2009.~--- P.~380---394.~--- (Lecture Notes in Computer Science; vol.~5407). % %In this paper we prove that the derivability problems for product-free Lambek calculus and product-free Lambek calculus allowing empty premises are NP-complete. %Also we introduce a new derivability characterization for these calculi. \bibitem{Savateev2009TCS} Savateev~Y\@. Unidirectional Lambek Grammars in Polynomial Time // Theory of Computing Systems.~--- 2009.~--- Vol.~46, \No~4.~--- P.~\mbox{662---672}. % %Lambek grammars provide a useful tool for studying formal and natural languages. %The generative power of unidirectional Lambek grammars equals that of context-free grammars. %However, no feasible algorithm was known for deciding membership in the corresponding formal languages. %In this paper we present a polynomial algorithm for deciding whether a given word belongs to a language generated by a given unidirectional Lambek grammar. \bibitem{Savateev2009EnVestnik} Savateev~Y\@. Recognition of derivability for the Lambek calculus with one division // Moscow University Mathematics Bulletin.~--- 2009.~--- Vol.~64, \No~2.~--- P.~\mbox{73---75}. % %Translation of \cite{Savateev2009Vestnik} \bibitem{Sorokin2011EnVestnik} Sorokin~A.~A.\@. The length of joins in Lambek calculus // Moscow University Mathematics Bulletin.~--- 2011.~--- Vol.~66, \No~3.~--- P.~\mbox{101---104}. % %Translation of \cite{Sorokin2011Vestnik} % %In 1992, M. Pentus established a criterion for the existence of a type $C$ such that for given types $A$ and $B$ the sequents $A \to C$ and $B \to C$ are derivable in the Lambek calculus. %In this paper we give an algorithm for construction of such a type $C$ (provided it exists) and prove a quadratic upper bound for its length. \bibitem{Sch1962} Sch\"{u}tte K\@. Der Interpolationssatz der intuitionistischen Pr\"{a}dikatenlogik // Mathematische Annalen.~--- 1962.~--- Vol.\ 148.~--- P.~192---200. \bibitem{Ter1999} Terui~K\@. Labelled tableau calculi generating simple models for substructural logics.~--- Amsterdam: Institute for Logic, Language and Computation, University of Amsterdam, 1999.~--- 19~p.~--- (ILLC Prepublication Series; \mbox{PP---1999---04}).~--- URL: \url{http://www.kurims.kyoto-u.ac.jp/~terui/lintab.pdf} (дата обращения: 22.03.2011). % Johan van Benthem % Йохан ван-Бентем \bibitem{vBen1983} Van Benthem~J\@. The semantics of variety in categorial grammar: Report \mbox{83---26}.~--- Department of Mathematics, Simon Fraser University, 1983.~--- Reprinted in Categorial Grammar / Editors W.~Buszkowski, W.~Marciszewski, J.~van~Benthem.~--- Amsterdam: John Benjamin, 1988.~--- P.~37---55. \bibitem{vBen1988} Van Benthem~J\@. Semantic parallels in natural language and computation.~--- Amsterdam: Institute for Logic, Language and Computation, University of Amsterdam, 1988.~--- 45~p.~--- (ILLC Prepublication Series; \mbox{LP---88---06}). \bibitem{vBen1989L} Van Benthem~J\@. Language in action // Journal of Philosophical Logic.~--- 1989.~--- Vol.~20.~--- P.~225---263. \bibitem{vBen1989S} Van Benthem~J\@. Semantic parallels in natural language and computation // Logic Colloquium. Granada 1987 / Editors H.-D.~Ebbinghaus et~al.~--- Amsterdam: North-Holland, 1989.~--- P.~\mbox{331---375}. \bibitem{vBen1991} Van Benthem~J\@. Language in Action: Categories, Lambdas and Dynamic Logic.~--- Amsterdam~etc.: North-Holland, 1991.~--- X,~350~p.~--- (Studies in Logic and the Foundations of Mathematics; vol.~130). \bibitem{Yet1990} Yetter D. N\@. Quantales and noncommutative linear logic // Journal of Symbolic Logic.~--- 1990.~--- Vol.~55, \No~1.~--- P.~41---64. \bibitem{Zie1981A} Zielonka~W\@. Axiomatizability of Ajdukiewicz--Lambek calculus by means of cancellation schemes // Zeitschrift f\"{u}r mathematische Logik und Grundlagen der Mathematik.~--- 1981.~--- Vol.~27, \No~3.~--- P.~215---224. \bibitem{Zie2009} Zielonka~W\@. Weak implicational logics related to the Lambek calculus~--- Gentzen versus Hilbert formalisms // Towards mathematical philosophy. Papers from the Studia Logica conference Trends in Logic IV / Editors D.~Makinson, J.~Malinowski, H.~Wansing.~--- Springer, 2009.~--- P.~201---212.~--- (Trends in Logic; vol.~28). \end{thebibliography}