ワークショップのお知らせ

<< IS COE Project: Verifiable and Evolvable e-Society >>

COE Workshop on Modal and Substructural Logics

(Final Announcement)

18th October (Mon), 2004 JAIST, Seminar Room, IS 3rd bldg. 6th floor

Program

9:30 - 10:20 J.M. Font (Univ. of Barcelona): Algebras and Models for Gentzen Systems

The algebraization of substructural logics that fits in the accepted frameworks has been usually done by considering a (structural) sentential logic having as theorems the desired logic, and applying to it more general methods. In this talk I will present an alternative framework which deals directly with the Gentzen systems and translates them into the equational consequence of a class of algebras. We will see that it is possible to develop a quite natural theory of matrices for Gentzen systems of the most general kind (i.e., either based on two-sided or on many-sided sequents, on hypersequents, etc.).

10:20 - 11:10 F. Bou (JAIST): Weak Heyting Algebras

The talk is devoted to explain several properties of the variety of weak Heyting algebras, which was introduced by Sergio Celani and Ramon Jansana. The interest of this variety comes from the fact that it gives a simultaneous treatment of the algebraic counterparts of modal logics and superintuitionistic logics, i.e., both the lattice of subvarieties of modal algebras and the lattice of subvarieties of Heyting algebras are complete sublattices of the lattice of varieties of weak Heyting algebras.

11:20 - 12:10 H. Ono (JAIST): On the Goedel Translation

Many of important logical consequences follow from the algebraization and parametrized local deduction theorem for substructural logics. For instance, classical embedding results by Glivenko or Kolmogorov are analyzed and extended much by using these algebraic tools (Galatos-Ono, in preparation). In the present talk, we will take up another classical embedding result given by the Goedel (or Goedel-McKinsey-Tarski) translation. A well- known theorem says that each superintuitionistic logic has "modal companions" among extensions of the modal logic S4. We will show that by the (slightly modified) Goedel translation each superintuitionistic logic can be embedded also into much weaker substructural modal logics. An embedding of intuitionistic logic into intuitionistic linear logic with exponential given by Girard is obtained as a special case.

Lunch

14:00 - 14:50 T. Litak (JAIST): The Importance of Being Discrete

The Kripke frames are very popular, intuitive and useful semantics for modal logics. Nevertheless, it is known that there are many systems which are Kripke-incomplete. It is of interest, then, to ask whether there is semantics more general than relational (i.e., Kripke) frames, but still non-trivial in the sense of being less general than boolean algebras with operators (BAOs). We would like to argue that particular attention should be devoted to discrete frames - i.e., general frames where all singletons are admissible. In many aspects, they seem to be better-behaved than another generalization of the Kripke frames: the neighbourhood frames (also known as Montague frames) or even than Kripke frames themselves. The talk will be centered around a characterization theorem obtained with Balder ten Cate (Amsterdam). We will show that completeness with respect to discrete frames is equivalent to many other, seemingly unrelated properties like certain form of algebraic completeness, admissibility of some non-standard rules or conservativity of so-called minimal hybrid extensions. This should provide us a good opportunity to say a few words on hybrid logic, which is one of the most interesting fields of research in contemporary modal logic. If time and space permits, we would also like to discuss and compare other generalizations of the notions of Kripke completeness, like neighbourhood completeness, conservativity of minimal tense extensions or completeness with respect to lattice-complete BAOs.

14:50 - 15:40 M. Zakharyaschev (King's College London): Reasoning about Distances and Topology

We propose a logic for reasoning about metric spaces with the induced topologies. It combines the `qualitative' interior and closure operators with `quantitative' operators `somewhere in the sphere of radius r,' including or excluding the boundary. We supply the logic with both the intended metric space semantics and a natural relational semantics, and show that the latter (i) provides finite partial representations of (in general) infinite metric models and (ii) reduces the standard `epsilon-definitions' of closure and interior to simple constraints on relations. These features of the relational semantics suggest a finite axiomatisation of the logic and provide means to prove its EXPTIME-completeness (even if the rational numerical parameters are coded in binary). An extension with metric variables satisfying linear rational (in)equalities is proved to be decidable as well. Our logic can be regarded as a `well-behaved' common denominator of logical systems constructed in temporal, spatial, and similarity-based quantitative and qualitative representation and reasoning. Interpreted on the real line (with its Euclidean metric), it is a natural fragment of decidable temporal logics for specification and verification of real-time systems. On the real plane, it is closely related to quantitative and qualitative formalisms for spatial representation and reasoning, but this time the logic becomes undecidable.

15:50 - 16:40 A. Kurucz (King's College London) : Higher Dimensional Products of Modal Logics

Products of modal logics were introduced in the 1970s and have been intensively studied ever since. Here we discuss the results and techniques concerning axiomatisation and decision problems for higher (>=3) dimensional product logics, and their connections to other many-dimensional formalisms, such as first-order classical and modal logics and algebraic logic.

========================================================================
The Workshop is organized by LCCC project team in JAIST, and is partly supported by JAIST International Joint Research Program and JSPS Invitation Program for British Professors.

For additional information, please contact

Hiroakira Ono : ono@jaist.ac.jp
Hitoshi Kihara : h-kihara@jaist.ac.jp