Name | Date | Size | ||
---|---|---|---|---|
.. | 25-Jul-2019 | 6 | ||
.gitignore | H A D | 25-Jul-2019 | 36 | |
CutFreeScript.sml | H A D | 25-Jul-2019 | 46.5 KiB | |
ExampleScript.sml | H A D | 25-Jul-2019 | 21.4 KiB | |
Holmakefile | H A D | 25-Jul-2019 | 902 | |
LambekScript.sml | H A D | 25-Jul-2019 | 93.4 KiB | |
README.md | H A D | 25-Jul-2019 | 796 |
README.md
1--- 2author: Chun Tian 3--- 4 5# A Formalized Lambek Calculus in Higher Order Logic \(HOL4\) 6 7based on an implementation of Lambek Calculus [1] in *Coq proof assistant* 8by **Houda ANOUN** and **Pierre CASTERAN** in 2003 [2]. 9 10The following is a brief listing of what's available in the distribution: 11 12- LambekScript.sml: Basic definitions and theorems of Lambek Calculus 13 14- CutFreeScript.sml: Properties of ���cut-free��� sequent proofs 15 16- ExampleScript.sml: Some examples 17 18Project paper is on arXiv: [https://arxiv.org/abs/1705.07318](https://arxiv.org/abs/1705.07318) 19 20**Related information** 21 22[1] Richard Moot and Christian Retor��. The Logic of Categorial 23Grammars: A Deductive Account of Natural Language Syntax and 24Semantics. Springer, 2012. 25 26[2] https://github.com/coq-contribs/lambek 27