coq-lambek

A Coq Toolkit for Lambek Calculus. This library contains some definitions concerning Lambek calculus. Three formalisations of this calculus are proposed, and also some certified functions which translate derivations from one formalism to another. Several derived properties are proved and also some meta-theorems. Users can define their own lexicons and use the defined tactics to prove the derivation of sentences in a particular system (L, NL, LP, NLP ...)

opam install coq-lambek.8.5.0
homepage
https://github.com/coq-contribs/lambek
license
LGPL 2
bugs tracker
https://github.com/coq-contribs/lambek/issues
dependencies
coq (>= 8.5 & < 8.6~)
source
https://github.com/coq-contribs/lambek/archive/v8.5.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-lambek/coq-lambek.8.5.0