|
Courses and Workshops
|
| Title: | Display logic meets categorial type logic |
| Lecturer(s): | Raffaella Bernardi (Free University of Bolzano-Bozen) and Rajeev Goré (Australian National University) |
| Type: | Advanced Course |
| Section: | Logic and Language |
| Week: | First | | Time: | 11.00-12.30 (Slot 2) |
| Webpage: | http://www.inf.unibz.it/~bernardi/ESSLLI04
|
| Reader: | Download | | Room: | C2 |
Description Standard presentations of Categorial Type Logic (CTL) using Gentzen's
Sequent Calculus or Proofnets are prototypical examples of a logical
account of natural language (NL) analysis. Nevertheless, the limitations
of these proof systems surface when one tries to fully explore the
'theoretical space' for type-logical connectives. We show how
the
generalised sequent framework of Display Calculi improves upon the
traditional accounts, and in particular, how it opens new perspectives
on the treatment of negative structure.
Such expressivity is required if one wants to enrich the type-logical
vocabulary with antitone connectives, in addition to the more familiar
isotone operations. Phenomena of polarity sensitivity, pervasive in
natural languages, suggest that such extensions are desirable.
Day One: we introduce Display Calculi as a unified framework for
presenting resource and structure sensitive reasoning.
Day Two: we show how CTL accounts for the composition of linguistic
resources while simultaneously allowing parsing, proving and the
construction of meaning.
Day Three: we weave these threads together by ``displaying''
CTLs. In
particular, we explain (i) how residuation forms the core of the system
giving rise to the categorial implications; (ii) how this naturally
generalises to n-ary operators; and (iii) how other alegbraic principles
can be encoded in CTL operators.
Day Four: we put n-ary operators to work, focusing on the use of upward
and downward entailing unary operators to account for sensitive items.
Day Five: we discuss how the proof-theoretical and model-theoretical
perspectives are related via basic soundness and completeness results,
and investigate the ``logical space'' for linguistic variation.
Further particulars
The course has goals at different levels. At the more concrete level,
the students will be smoothly introduced to multi-modal categorial
logic. They will learn how the system is logically engineered for
linguistic applications, and learn how Display Calculi provide a uniform
framework for understanding the unary and binary operators seen at work
in these applications. At the second level, they will actually learn
about display calculi per se. And in the process, at the most abstract
level, they will receive hands-on experience on logic engineering.
The course is addressed to any student interested in logic, language and
their connections, and only basic background on propositional logic is
required. Students with knowledge of categorial grammar and proof theory
will, of course, obtain further profit.
The course can be seen as a continuation of the foundational course on
"Substructural Logics" given by Greg Restall at ESSLLI 01
(Helsinki)
--see: http://www.folli.uva.nl/CD/2001/courses/itsl.html. In particular,
we will show substructural logics at work by focusing on a specific one
(CTL) and by zooming in on the linguistic applications only mentioned by
Restall.
There are no textbooks on the connection between DL and CTL, hence no
comparison is possible. We will provide all the required course material
which will be mostly based on the references below:
* R. Bernardi, Reasoning with Polarity in Categorial Type Logic. PhD
Thesis, UiL OTS, 2002.
* R. Gore, Substructural Logics on Display. Logic Journal of the
Interest Group in Pure and Applied Logics. 6(3):451-504, 1998.
* G. Restall, An Introduction to Substructural Logics. Routledge,
2000.
|
© 2003, 2004 LORIA, Carlos Areces. |
2004-04-07
| |
