On the complexity of the Lambek-Grishin calculus
Summary
The Lambek-Grishin calculus LG is the symmetric extension of the non-associative Lambek calculus NL. In this thesis we prove that the derivability problem for LG and the product-free fragment of LG is NP-complete. In the second part of the thesis an implementation of a theorem prover for LG is discussed.