Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
A Coq Toolkit for Lambek Calculus
Fetching latest commit…
Cannot retrieve the latest commit at this time.
|Type||Name||Latest commit message||Commit time|
|Failed to load latest commit information.|
================================ Readme ================================ =========================================== Name : Lambek-Calculus Title: A Coq toolkit for Lambek Calculus Authors: Houda ANOUN & Pierre CASTERAN Institution: LaBRI , Bordeaux Date : March - July 2003 =========================================== Description: ------------ 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 ...) Keywords: Computational linguistic, categorial grammar, Lambek Calculus... -------- Interested users can find more details about this library in the INRIA research report titled 'Logical Toolkit for Lambek Calculus' Files contents : =============== Form.v : axiomatic presentation of Lambek Calculus Semantics.v & Filters.v : proof that axiomatic presentation is sound and complete (using Kripke Models) Sequent.v : sequent calculus ReplaceProp.v : some properties of the predicate 'replace' NaturalDeduction.v: natural deduction Polarity.v: Polarity meta-theorem CutSequent.v:sub-formula property LSeqProp.v : some properties concerning L system Tactics.v : some tactics defined in Ltac language Example*.v : some examples ArrowDed.v: functions that translate derivations from the axiomatic presentation to natural deduction formalism and conversely ArrowGentzen.v:functions that translate derivations from gentzen calculus to axiomatic presentation and conversely GentzenDed.v:functions that translate derivations from gentzen calculus to natural deduction formalism and conversely