NameDateSize

..25-Jul-20196

.gitignoreH A D25-Jul-201936

CutFreeScript.smlH A D25-Jul-201946.5 KiB

ExampleScript.smlH A D25-Jul-201921.4 KiB

HolmakefileH A D25-Jul-2019902

LambekScript.smlH A D25-Jul-201993.4 KiB

README.mdH A D25-Jul-2019796

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