Keywords: Interactive Theorem Proving, Proof Mechanisation, Higher Order Logic, NLP
Units: 12/24 units
Background
Categorial grammars (see [Moot] and also [vanBenthem]) and the Categorial Type Logics are lexcalized grammars, as opposed to the phrase structure grammars like context-free grammars that were introduced afterwards. Although the success of phrase structure grammars went far beyond that of categorial grammars, their lexicalization was in fact an attractive feature, another one being their connection to logical semantics.
Lambek calculus (see also [Moot]) enables a completely logical treatment of categorial grammar. The theorem of Pentus has established the weak equivalence between context-free grammars and Lambek grammars.
Research Questions and Tasks
This project is an opportunity for students who wants to learn the HOL4 theorem-proving system by extending the existing formalization of Lambek calculus in HOL’s official examples). The existing work was ported from Coq, where the proof of the important Cut-Elimination Theorem for Lambek Calculus is also not finished. This project will include the following tasks:
- Finish the proof of the Cut-Elimination Theorem for Lambek Calculus.
- Mechanise Pentus’s proof on the weak equivalence between context-free grammars (CFG) and Lambek grammars. (NOTE: HOL already has formalizations of CFG grammar as part of official examples, we want to make a connection between it and the one for Lambek calculus.)
- (for 24 credits/units) Implement a decision procedure in HOL, based on the Cut-Elimination Theorem, to automatically decide and deduce the grammar structure of any given lexicals and sample sentences.
The development should follow modern techniques and guidelines for HOL4, e.g. [HOLTutorial] and [HOL4]. Ideally, the project will be submitted to HOL4 official as part of its core theories.
NOTE: The student will get some basic training through a mini course to get familar with interactive theorem proving (ITP) techniques (and HOL4 in particular).
References
- [HOLTutorial] The HOL System LOGIC
- [HOL4] The HOL System DESCRIPTION
- [Moot] Moot, R., Retore, C.: LNCS 6850 - The Logic of Categorial Grammars. Springer Berlin Heidelberg, Berlin, Heidelberg (2012).
Requirements:
Basic knowledge of formal logic and lambda-calculus (simple typed); some experiences with interactive theorem provers; basic knowledeg of natural language processing.