SLACS 2006
Program
9月11日
- 10:00--10:40 中澤巧爾 (京都大学)
-
A subsystem of sequent calculus isomorphic to natural deduction
シーケント計算のカット除去と自然演繹の正規化との関連について。
- 10:50--11:30 小島健介 (京都大学)
-
Kleese's slash interpretationの統一的記述について
Kleene's slash interpretationは直観主義論理におけるdisjunctionとexistenceの性質を調べるために導入された解釈の一つである。その定式化は対象となる体系ごとに別々に行われていたが、これを統一的に記述することができないかを一階の体系に限定して考察する。
- 11:40--12:20 宮崎裕 (北海道大学)
-
The upper part of the lattice NEXT(KTB)
We will describe the structure of the upper part of the lattice of normal modal logics containing KTB, and discuss some related problems.
- 14:30--15:10 佐野勝彦 (京都大学)
-
A Hybridization of Irreflexive Modal Logics
Unlike ordinary modal language, hybrid language makes it possible to refer to states (possible worlds) in formulas. This is achieved by a class of formulas called nominals. This talk discusses hybrid language with a sub-modality (called the irreflexive modality) associated with the intersection of the accessibility relation R and the inequality. First, we provide the Hilbert-style axiomatizations (with and without the Gabbay-style rule) for logics of our language, and prove the Kripke completeness. Second, with respect to the frame expressive power, we compare the effect of the irreflexive modality with that of nominals. Finally, we establish the Goldblatt-Thomason-style characterization for our language.
- 15:20--16:00 鈴木徹 (東京工業大学)
-
様相定数を含む様相論理について
- 16:10--16:50 川本裕輔 (東京大学)
-
知識論理による匿名性検証のための関数部分知識モデル
- 17:00--17:40 関隆宏 (九州大学)
-
Some classes of relevant modal logics
メタ完全な適切論理は構文論的な面から2種類に分類できることが知られている。適切様相論理に対してこのような分類が可能であるか、あるいは別の側面から分類できるかどうかについて考えていく。
- 17:45-- 安部達也 (東京大学)
- (Informal session)
9月12日
- 10:00--10:40 角谷良彦 (東京大学)
-
Calculi and semantics for normal modal logics
We provide a calculus for the intutionistic modal logic IK and its categorical semantics. We also show variations of calculi for the classical modal logic K.
- 10:50--11:30 Paul-Andre Mellies (CNRS / Universite Paris 7)
-
Functorial boxes in string diagrams
String diagrams were introduced by Roger Penrose
as a handy notation to manipulate morphisms in a monoidal category.
In principle, this graphical notation should encompass the various
pictorial systems introduced in proof-theory (like Jean-Yves Girard's
proof-nets) and in concurrency theory (like Robin Milner's bigraphs).
This is not the case however, at least because string diagrams do not
accomodate boxes --- a key ingredient in these pictorial systems.
In this short tutorial talk, based on our accidental rediscovery
of an idea by Robin Cockett and Robert Seely, we explain how string
diagrams may be extended with a notion of functorial box to depict
a functor separating an inside world (its source category)
from an outside world (its target category).
Then, we expose two elementary applications of the notation:
first, we characterize graphically when a faithful balanced monoidal
functor F : C -> D transports a trace operator from the category D
to the category C, and exploit this to construct well-behaved
fixpoint operators in cartesian closed categories generated
by models of linear logic; second, we explain how the categorical
semantics of linear logic induces that the exponential box
of proof-nets decomposes as two enshrined boxes.
- 11:40--12:20 龍田真 (国立情報学研究所)
-
代入定理
ラムダ計算において、項Mが、その中の変数x1, ... xnに対して任意の1個の強正規化可能な項Xを代入したものM[x1:=X, ..., xn:=X]が常に強正規化可能であれば、その中の変数x1, ... xnに対して任意のn個の強正規化可能な項X1, ..., Xnをそれぞれ代入したものM[x1:=X1, ..., xn:=Xn]も常に強正規化可能であることを示す。これを応用して、永続強正規化可能性を共通型をもつ型理論HLによる特徴付けを与え、Theoretical Computer Scienceに2005年に提出された未解決問題を解いた。これは、Mariangiola Dezaniとの共同研究である。
- 14:30--15:10 高穎 (埼玉大学)
-
Operations and Relations: Two Semantical Treatments of Intensional Connectives in Non-Classical Logics
In non-classical logics, there are many intensional connectives, which can be modeled by operations and/or relations. For example, there are two similar semantics for relevant logics, both of which are developments of Alasdair Urquhart’s “semilattice semantics”. One is the well-known ternary relation semantics. The other is Kit Fine’s semantics, which uses a binary operation to model implication. In his Gaggle theory, Dunn has provided a uniform semantical approach to a variety of logics, by using n+1 placed relations to interpret n placed connectives. Motivated by Dunn’s theory and Fine’s semantics for relevant logics, the goal of our research work is to find a uniform semantical approach to n placed connectives by n placed operations, and to investigate the relationship between Dunn’s and our approaches. The main contribution of our work is to give a good understanding of the link between these two semantical treatments.
- 15:20--16:00 倉田俊彦 (法政大学)
-
Some aspects of extensionality of arrows in cartesian closed category
単純型付ラムダ計算のモデルについて，既知の枠組みの外延性に関する特徴をまとめる．特に，カルテシアン閉圏において，ラムダ定義可能な射の外延性について考察する．
- 16:10--16:50 野口真理子 (奈良女子大学)
-
Prologによるmakeの実装 〜Mipl〜
我々はPrologによってmakeを再実装するプロジェクト「mipl」を進行中である。現在のmakeの代用に耐えうるよう、OSのコンパイルが可能である程度のものを目標としている。Prologを実装言語に用いることにより、データ構造を明確に記述することが可能となる。また、機能の追加をライブラリ形式にすることで現在のmakeのような種類の氾濫をを防ぐ。本発表ではこれまでの設計方針と進行状況について述べる。
- 17:00--17:40 星野直彦 (京都大学)
-
純粋に線形なラムダ計算のAbadi-Plotokin logic
!を含まない純粋に線形なラムダ計算のAbadi-Plotokin logicを定義して無限個の項を持つ型の具体例を紹介する。