Proving theorems of the second order Lambek calculus in polynomial time |
| |
Authors: | Erik Aarts |
| |
Affiliation: | (1) Research Institute Language and Speech, Utrecht University, Trans 10, 3512 JK Utrecht, The Netherlands;(2) Dept. of Mathematics and Computer Science, University of Amsterdam, Plantage Muidergracht 24, 1018 TV Amsterdam, The Netherlands |
| |
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.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).Presented byCecylia Rauszer |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|