|
Courses and Workshops
|
| Title: | Proof automation for type-logical grammars |
| Lecturer(s): | Pierre Castéran (Université Bordeaux I, Inria Futurs) and Richard Moot (Université Bordeaux I) |
| Type: | Introductory Course |
| Section: | Logic and Computation |
| Week: | Second | | Time: | 14.00-15.30 (Slot 3) |
| Webpage: | http://www.labri.fr/Perso/~casteran/
|
| Reader: | Download | | Room: | CR |
Description Type-logical grammars are an attractive way of developing grammars in a
mathematically precise way. In this course we will use automated and
semi-automated logical tools to prove theorems both about and of the
multimodal Lambek calculus.
In the first week we will show how to use Coq to prove several of the
standard theorems about the multimodal Lambek calculus: soundness and
completeness with respect to the models and the equivalence of different
presentations of the calculus (axiomatic, natural deduction, sequent).
The second week will be dedicated to automated theorem proving in the
multimodal Lambek calculus. We will look at a new implementation of the
Grail theorem prover and the underlying technology: maintaining the
transitive closure of a changing graph (dynamic transitive closure) and
sharing subtrees in the derivation whenever possible.
On the practical side, the students will use the computational tools of
this course to prove some elementary theorems.
/Further particulars/
The students should have some knowledge on Lambek calculus or on proof
assistants (both are better, but not mandatory)
|
© 2003, 2004 LORIA, Carlos Areces. |
2003-11-20
| |
