Abstract
In the Lambek calculus of order 2 we allow only sequents in which the depth of nesting of implications is limited to 2. We prove that the decision problem of provability in the calculus can be solved in time polynomial in the length of the sequent. A normal form for proofs of second order sequents is defined. It is shown that for every proof there is a normal form proof with the same axioms. With this normal form we can give an algorithm that decides provability of sequents in polynomial time.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
W. Buszkowski,On generative capacity of the Lambek calculus, paper presented at JELIA '90: Logics in AI, Amsterdam 1990.
T. H. Cormen, C. E. Leiserson, andR. L. Rivest Introduction to algorithms MIT Press, Cambidge, MA 1990.
H. Hendriks,Lambek Semantics, paper presented at 8th Amsterdam Colloquium, Amsterdam 1992.
J. Lambek,The Mathematics of Sentence Structure American Mathematical Monthly 65, 1985, pp. 154–169.
M. Moortgat,Categorial Investigations. Logical and Linguistic Aspects of the Lambek Calculus, Universiteit van Amsterdam, Dissertation 1988.
M. Pentus,Lambek Grammars are Context-free, paper presented at Workshop on Grammar, Proof theory and Complexity, Amsterdam 1993.
D. Roorda,Resource Logics: Proof-theoretical Investigations, Universiteit van Amsterdam, Dissertation 1991.
Author information
Authors and Affiliations
Additional information
The author was sponsored by project NF 102/62–356 (‘Structural and Semantic Parallels in Natural Languages and Programming Languages’), funded by the Netherlands Organization for the Advancement of Research (NWO).
Rights and permissions
About this article
Cite this article
Aarts, E. Proving theorems of the second order Lambek calculus in polynomial time. Stud Logica 53, 373–387 (1994). https://doi.org/10.1007/BF01057934
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF01057934