% lcr.bbl % Mati Pentus, 2006/12/04, 2016/06/26 % 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}. %???55---57 [springerlink.com] % %В статье предъявляется подстановка, сводящая выводимость в исчислении Ламбека с единицей с одним делением к выводимости в исчислении Ламбека с одним делением, допускающем пустые антецеденты. %При помощи этой подстановки устанавливается существование алгоритма, за полиномиальное время проверяющего выводимость в исчислении Ламбека с единицей с одним делением. \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}. % % В~статье рассматриваются двусторонние идеалы полуколец. Изучается теория двусторонних идеалов в~сигнатуре, состоящей из предикатного символа~$ \subseteq $ и двух функциональных символов, обозначающих правое деление и левое деление идеалов. Доказывается, что множество атомарных формул этой сигнатуры, истинных на всех полукольцах при всех оценках, разрешимо. \bibitem{Pentus2009FPM} Пентус~А.~Е., Пентус~М.~Р\@. Атомарная теория умножения и деления двусторонних идеалов полуколец // Фундаментальная и прикладная математика.~--- 2009.~--- Т.~15, \No~2.~--- С.~\mbox{169---189}. % % В~статье рассматриваются двусторонние идеалы полуколец. Изучается теория двусторонних идеалов в~сигнатуре, состоящей из предикатного символа~$ \subseteq $ и трёх функциональных символов, обозначающих умножение, правое деление и левое деление идеалов. Доказывается, что множество атомарных формул этой сигнатуры, истинных на всех полукольцах при всех оценках, разрешимо. \bibitem{Pentus2012FPM} Пентус~А.~Е., Пентус~М.~Р\@. Атомарная теория левого деления двусторонних идеалов полуколец с единицей // Фундаментальная и прикладная математика.~--- 2011/2012.~--- Т.~17, \No~5.~--- С.~\mbox{129---146}. % % В~статье рассматриваются двусторонние идеалы полуколец с~единицей. Изучается теория двусторонних идеалов в~сигнатуре, состоящей из двуместного предикатного символа, обозначающего отношение \lk быть подмножеством\pk, и двуместного функционального символа, обозначающего левое деление идеалов. Доказывается, что пробема распознавания истинности атомарной формулы этой сигнатуры на всех полукольцах с~единицей при всех оценках, разрешима за полиномиальное время. Аналогичный результат верен для атомарных формул с~правым делением, но без левого деления. \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{Savateev2011} Саватеев~Ю.~В\@. Применение сетей доказательств для исследования фрагментов исчисления Ламбека // Изв. РАН. Сер. матем.~--- 2011.~--- Т.~75, \No~3.~--- С.~\mbox{189---222}. % %В данной работе с помощью сетей доказательств исследуется алгоритмическая сложность проблемы выводимости в некоторых фрагментах исчисления Ламбека. %Доказана NP-полнота этой задачи для одностороннего фрагмента и для фрагмента без умножения, а также для вариантов этих фрагментов, допускающих пустые антецеденты. \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{Kuznetsov2011EnVestnik} Kuznetsov~S.~L\@. Lambek calculus with a unit and one division // Moscow University Mathematics Bulletin.~--- 2011.~--- Vol.~66, \No~4.~--- P.~\mbox{173---175}. %??? \bibitem{Kuznetsov2012IGPL} Kuznetsov~S\@. Lambek grammars with one division and one primitive type // Logic Journal of the IGPL.~--- 2012.~--- Vol.~20, \No~1.~--- P.~\mbox{207---221}. % %We prove that a formal language without the empty word is context-free if and only if it is generated by some $\mathrm{L}(\bs; p_1)$-grammar, where $\mathrm{L}(\bs; p_1)$ is the Lambek calculus with one division and one primitive type. %To do that, we use a substitution of types which reduces derivability in $\mathrm{L}(\bs)$ to derivability in $\mathrm{L}(\bs;p_1)$. %We also prove that a formal language (possibly, with the empty word) is context-free if and only if it is generated by some $\mathrm{L}^{\!*}(\bs;p_1)$-grammar (where $\mathrm{L}^{\!*}(\bs;p_1)$ is a variant of $\mathrm{L}(\bs;p_1)$ that allows empty premises). %To do that, we introduce a construction which adds the empty word to languages generated by a special subclass of $\mathrm{L}^{\!*}(\bs)$-grammars (which covers all context-free languages without the empty word) and then use the same substitution as for $\mathrm{L}(\bs)$. \bibitem{Kuznetsov2012LACL} Kuznetsov~S\@. L-completeness of the Lambek calculus with the reversal operation // Logical Aspects of Computational Linguistics, 7th International Conference, LACL 2012, Nantes, France, July 2---4, 2012. Proceedings / Editors D.~B\'echet and A.~Ja.~Dikovsky.~--- Berlin: Springer, 2012.~--- P.~151---160.~--- (Lecture Notes in Computer Science; vol.~7351). % %We extend the Lambek calculus with rules for a unary operation corresponding to language reversal and prove that the new calculus is complete with respect to the class of models on subsets of free semigroups (L-models). %We also prove that categorial grammars based on this calculus generate precisely all context-free languages. \bibitem{Kuznetsov2014LNCS8222} Kuznetsov~S\@. L-completeness of the Lambek calculus with the reversal operation allowing empty antecedents // Categories and Types in Logic, Language, and Physics / Editors C.~Casadio, B.~Coecke, M.~Moortgat, and P.~Scott.~--- Heidelberg: Springer, 2014.~--- P.~\mbox{268---278}.~--- (Lecture Notes in Computer Science; vol.~8222). % %In this paper we prove that the Lambek calculus allowing empty antecedents and enriched with a unary connective corresponding to language reversal is complete with respect to the class of models on subsets of free monoids (L-models). \bibitem{Kuznetsov2017arXiv} Kuznetsov~S\@. The Lambek calculus with iteration: two variants [Электронный ресурс].~--- 2017.~--- Режим доступа: arXiv:1705.07309 % %Formulae of the Lambek calculus are constructed using three binary connectives, multiplication and two divisions. We extend it using a unary connective, positive Kleene iteration. For this new operation, following its natural interpretation, we present two lines of calculi. The first one is a fragment of infinitary action logic and includes an omega-rule for introducing iteration to the antecedent. We also consider a version with infinite (but finitely branching) derivations and prove equivalence of these two versions. In Kleene algebras, this line of calculi corresponds to the *-continuous case. For the second line, we restrict our infinite derivations to cyclic (regular) ones. We show that this system is equivalent to a variant of action logic that corresponds to general residuated Kleene algebras, not necessarily *-continuous. Finally, we show that, in contrast with the case without division operations (considered by Kozen), the first system is strictly stronger than the second one. To prove this, we use a complexity argument. Namely, we show, using methods of Buszkowski and Palka, that the first system is $\Pi_1^0$-hard, and therefore is not recursively enumerable and cannot be described by a calculus with finite derivations. \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). \bibitem{Pentus2014LNCS8222} Pentus~M\@. The monotone Lambek calculus is NP-complete // Categories and Types in Logic, Language, and Physics / Editors C.~Casadio, B.~Coecke, M.~Moortgat, and P.~Scott.~--- Heidelberg: Springer, 2014.~--- P.~\mbox{368---380}.~--- (Lecture Notes in Computer Science; vol.~8222). % %We consider the Lambek calculus with the additional structural rule of monotonicity (weakening). %We show that the derivability problem for this calculus is NP-complete (both for the full calculus and for the product-free fragment). %The same holds for the variant that allows empty antecedents. %To prove NP-hardness of the product-free fragment, we provide a~mapping reduction from the classical satisfiability problem $ \textit{SAT} $. %This reduction is similar to the one used by Yury Savateev in 2008 to prove NP-hardness (and hence NP-completeness) of the product-free Lambek calculus. % 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} % %A polynomial algorithm for determination of derivability in the Lambek calculus with one division is described in the paper. \bibitem{Savateev2011En} Savateev~Y\@. An application of proof-nets to the study of fragments of the Lambek calculus // Izv.\ Math.~--- 2011.~--- Vol.~75, \No~3.~--- P.~\mbox{631---663}. % %Translation of \cite{Savateev2011} % %We use proof-nets to study the algorithmic complexity of the derivability problem for some fragments of the Lambek calculus. %We prove the NP-completeness of this problem for the unidirectional fragment and the product-free fragment, and also for versions of these fragments that admit empty antecedents. \bibitem{Savateev2012APAL} Savateev~Y\@. Product-free Lambek calculus is NP-complete // Annals of Pure and Applied Logic.~--- 2012.~--- Vol.~163, \No~7.~--- P.~\mbox{775---788}. %The Symposium on Logical Foundations of Computer Science 2009. %Editors S.~N.~Artemov and A.~Nerode. % %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{Sch1962} Sch\"{u}tte K\@. Der Interpolationssatz der intuitionistischen Pr\"{a}dikatenlogik // Mathematische Annalen.~--- 1962.~--- Vol.\ 148.~--- P.~192---200. \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{Sorokin2012} Sorokin~A\@. On the completeness of Lambek calculus with respect to cofinite language models // Logical Aspects of Computational Linguistics, 7th International Conference, LACL 2012, Nantes, France, July 2---4, 2012. Proceedings / Editors D.~B\'echet and A.~Ja.~Dikovsky.~--- Berlin: Springer, 2012.~--- P.~229---233.~--- (Lecture Notes in Computer Science; vol.~7351). % %We give an alternative proof of the fact that the product-free Lambek calculus is complete with respect to cofinite language models. %It was first proved by Buszkowski in 1982 by the method of barriers. %We use another method, which is also based on the technique of canonical models, to obtain a new proof of this result. \bibitem{Sorokin2014LNCS8222} Sorokin~A\@. Conjoinability in 1-discontinuous Lambek calculus // Categories and Types in Logic, Language, and Physics / Editors C.~Casadio, B.~Coecke, M.~Moortgat, and P.~Scott.~--- Heidelberg: Springer, 2014.~--- P.~\mbox{393---401}.~--- (Lecture Notes in Computer Science; vol.~8222). % %In the present work we prove a conjoinability criterion for $1$-discontinuous Lambek calculus. %It turns out that types of this calculus are conjoinable if and only if they have the same sort and the same interpretation in the free abelian group generated by the primitive types. \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}