プログラム

今回の「記号論理と情報科学'95」と「証明論'95」は共同開催で、4日間で、 計9個のセッションを行ないます。各セッションの日程は、以下のスケジュー ル表をご覧になって下さい。

また各セッションにて行なわれる講演の詳細な情報(講演時間や題目など)につ きましては、アブストラクト集にございますので、そちらをご覧になって下さ い。

<<<< スケジュール表 >>>>

(Continued)

[xxx] は会場となる講義室の番号を示します。
(ex. [501] → 講義棟 501 講義室 )

アブストラクト集

Session 1B --- 9/17(Sun) PM: SLACS ---

セッション１Ｂ ---9月17日(日) 午後: SLACS---

 
 13:30 		 		 		  Opening

 13:40 - 14:10 		 		 鴨 浩靖 ::

    		 論理プログラムの開項Herbrand解釈を用いた意味論について

 14:10 - 14:20 		 		 		  break

 14:20 - 14:50 		 		 Jacques Garrigue::

    		 トランスフォーメーション計算系と直観主義線形論理

 14:50 - 15:20 		 		 		  coffee break

 15:20 - 15:40 		 		 沢村 一 ::

    		 線形論理を用いた並行度解析

    		 		 - Gunter & Gehlot論文の訂正とコメント -

 15:40 - 15:50 		 		 		  break

 15:50 - 16:20 		 		 山崎 勇 ::

    		 推論加群系とその応用

 16:20 - 16:30 		 		 		  break

 16:30 - 17:00 		 		 竹内 泉 ::

    		 パラメトリシティーの為の論理体系の実現可能性解釈

{} アブストラクト
------------------------Session 1B(9/17(Sun)) PM: SLACS---
講演者
鴨 浩靖 (KAMO, Hiroyasu)
所属
奈良女子大学 理学部 情報科学科
講演日時
9/17(Sun) 13:40 - 14:10 (30min.)
講演題目
論理プログラムの開項Herbrand解釈を用いた意味論 について
Title
On the Semantics of Logic Programs with Open-Term Herbarnd Interpretations
アブストラクト
ある一階言語の開項Herbrand解釈とは、その言語のすべての項の集合 を領域とする解釈のことである。論理プログラムの開項Herbrand 解 釈を用いた意味論について調べ、Herbrand解釈を用いた意味論や他の いくつかの意味論と比較する。
Abstract
The open-term Herbrand interpretation of a first-order language is the interpretation with the set of all terms in the language as its universe. We investigate the semantics of logic programs with the open-term Herbrand interpretations and compare it with the semantics with the Herbrand interpretations and some other semantics.

------------------------Session 1B(9/17(Sun)) PM: SLACS---
講演者
Jacques Garrigue
所属
京都大学 数理解析研究所
講演日時
9/17(Sun) 14:20 - 14:50 (30min.)
講演題目
トランスフォーメーション計算系と直観主義線型論理
Title
Transformation Calculus and ILL
アブストラクト
通常の計算にラベルつきの抽象と合成を導入したトラン スフォーメーション計算系のコンビネータ版はＩＬＬと深い関係をもっ ている。特に面白いのは、直観主義論理と計算のカリー・ ハワード同形において変数名が果している役割は、今度ラベルが果す ことになり、ＴＣの合成の線型性が明らかになる。
Abstract
Transformation Calculus and ILL A combinatorial formulation of transformation calculus, an extension of lambda calculus with labeled parameters and labeled multi-composition, appears to be in a strong relationship with the intuitionistic linear logic. Particularly, where the Curry-Howard isomorphism uses variables, we use labels, and the distinction shows the linearity of TC's composition.

------------------------Session 1B(9/17(Sun)) PM: SLACS---
講演者
沢村 一 (Sawamura, Hajime)
所属
(株) 富士通研究所 情報社会科学研究所
講演日時
9/17(Sun) 15:20 - 15:40 (20min.)
講演題目
線形論理を用いた並行度解析 --- Gunter & Gehlot 論文の訂正とコメント ---
Title
Analyzing degree of concurrency by linear logic
--- corrections and comments on Gunter & Gehlot's paper ---
アブストラクト
並行計算の並行度を高める計算スケジュールは並列・分散計算などに おける最も重要な課題の一つである。Gunter & Gehlotはペトリネッ トによる並行計算と線型論理の証明との同一視に基づき、並行計算の 並行度を証明からある種のカットを除去することで高めるという大変 興味深い方法を与えている。本講演では、この方法に含まれる、致命 的ではないが基本的な誤りを指摘し、コメントを加える。またこの方 法の今後の展開についても議論する。
Abstract
Raising degree of concurrency is one of the most important questions in pararell and distributed computing. Based on the identification of Petri net computations with linear logic proofs, Gunter and Gehlot devised such a very intriguing method that the degree of concurency in a concurrent computation can be raised by eliminating particular cuts from the corresponding proof. In this talk, we will point out not a fatal but basic error and add some comments. We also discuss further developments of this method.

------------------------Session 1B(9/17(Sun)) PM: SLACS---
講演者
山崎 勇 (Yamazaki, Isamu)
所属
(株) 東芝 研究開発センター 情報・通信システム研究所
講演日時
9/17(Sun) 15:50 - 16:20 (30min.)
講演題目
推論加群系とその応用
Title
An Inference Module System and its expected applications
アブストラクト
一階述語論理に於ける、推論加群系と名付けた、ほとんど線形空間系 と同様の扱いができる代数系と、その応用の可能性を紹介する。推論 加群系は、導出などの推論を２項演算化して導かれる加群（推論加群） と、その係数環、更にその双対加群である事実加群などからなる。例 えば節集合の充足可能性問題は推論加群系の上での一次方程式の非負 の解の存在問題となる。また推論加群から推論加群への準同形写像は 理論の相似性を、また同形写像は理論の等価性を、調べる手段となり 得る。
Abstract
The auther propose a new algebraic system, named Inference Module System, which includes, ring R, right R module D (named Inference module), and left R module Psi (named Fact Module). Each of D and Psi is (subset of) the dual module of the other. They are almost dual linear spaces with infinite dimension. Further, the notion of "satisfy"(|=) in FOL can be expressible in algebraic formula using these modules. And the addition in D can be interpreted as sound inference in FOL. As one example, the Algebraic Proving Principle holds, which states that when generarized Horn condition holds, a set of clauses is unsatisfiable iff a lenear equation ("proving equation" derived from the clause set) has a non-negative solution. Homomorphisms in this sysytem are expected to become effective tools for studying analogy or equality between theories.

------------------------Session 1B(9/17(Sun)) PM: SLACS---
講演者
竹内 泉 (Takeuti, Izumi)
所属
東京都立大学 理学部
講演日時
9/17(Sun) 16:30 - 17:00 (30min.)
講演題目
パラメトリシティーの為の論理体系の実現可能性解釈
Title
アブストラクト
プロトキンらによって提案されたパラメトリシティーの為の論理体系 に対し、健全かつ完全な実現可能性解釈があることを示す。
Abstract
Plotkin and Abadi proposed a logical system for parametricity. We give it a sound and cmplete realizability interpretation.

Session 2A ---9/18(Mon) AM: Proof Theory---

セッション２Ａ ---9月18日(月) 午前: Proof Theory---

 
 10:00 		 		 		  Opening

 10:10 - 11:00 		 		 金子 守、永島 孝 ::

    		 Game logic and its applications II

 11:00 - 11:10 		 		 		  break

 11:10 - 11:30 		 		 竹内 泉、広川 左千夫 ::

    		 A functional calculus of implication

 11:30 - 11:40 		 		  break

 11:40 - 12:25 		 		 高木 理 ::

    		 dilator と loh-functor

 12:25 - 13:20 		 		 		  Lunch

{} アブストラクト
------------------------Session 2A(9/18(Mon)) AM: Proof Theory---
講演者
金子 守* (Kaneko, Mamoru)、
永島 孝** (Nagashima, Takashi)
所属
(*) 筑波大学 社会工学系、
(**) 一橋大学 数学教室
講演日時
9/18(Mon) 10:10 - 11:00 (50min.)
講演題目
Game logic and its applications II
Title
Game logic and its applications II
アブストラクト
この論文の Part I では、Game Logic framework は Hilbert style で与えた。この Part II では、それらを Gentzen style sequent calculi で与える。そして、それらの体系で Cut-Elimination Theorem を証明し、Part I での game theoretical undecidability Theorem の証明に使った Term Existence Theoremを証明する。
Abstract
This paper provides a Gentzen style formulation of our game logic framework , and proves the cut-elimination theorem for . As its applications, we prove the term existence theorem for used in Part I.

------------------------Session 2A(9/18(Mon)) AM: Proof Theory---
講演者
竹内 泉* (Takeuti, Izumi)、
広川 左千夫** (Hirokawa, Sachio)
所属
(*) 東京都立大学 理学部、
(**) 九州大学 理学部
講演日時
9/18(Mon) 11:10 - 11:30 (20min.)
講演題目
A funcutional calculus of implication
Title
A funcutional calculus of implication
アブストラクト
Abstract

Typed lambda-calculus and category theory are the two sides of the same coin. We describe a formal system for the implicational fragment of intuitionistic logic which, we think, corresponds to arrow only category. The idea is to use the rule of composition:



instead of the rule of modus ponens:



------------------------Session 2A(9/18(Mon)) AM: Proof Theory---
講演者
高木 理 (TAKAKI, Osamu)
所属
京都産業大学 理学研究科 数学専攻
講演日時
9/18(Mon) 11:40 - 12:25 (45min.)
講演題目
dilator と loh-functor
Title
Dilator and loh-functor
アブストラクト
ordinal x,yに対しxからyへの強順序保存関数全体に適当なlinear orderを与え, これをloh(x,y)とする。また、与えられたordinal xに 対して, ONからOLへのfunctorでordinal yをloh(x,y)に写すものを loh(x,-)-functorとする。これがdilatorになる為の条件、および loh-functorによるdilatorの構成について述べる。
Abstract
For any ordinal x,y, let loh(x,y) be a linear ordered set of strictly increasing functions mapping x to y. For any x, we define a functor loh(x,-) which maps an ordinal y to loh(x,y). We show that for any n in loh(n,-) is a dilator. And we consider a construction of dilators with loh-functors.

Session 2B ---9/18(Mon) AM: SLACS---

セッション２Ｂ ---9月18日(月) 午前: SLACS---

 
 10:15 - 10:50 		 		 小林 聡 ::

     		 Type Theory with Evaluation Modalities

 10:50 - 11:00  		 		 		  break

 11:00 - 11:35  		 		 林 晋 ::

     		 ctPX and mvPX: two extensions of PX

 11:35 - 11:45  		 		 		  break

 11:45 - 12:20  		 		 小林 孝次郎 ::

     		 universal distribution の malignness を保存する変換について

 12:20 - 13:20  		 		 		  Lunch

{} アブストラクト
------------------------Session 2B(9/18(Mon)) AM: SLACS---
講演者
小林 聡 (Kobayashi, Satoshi)
所属
龍谷大学 理工学部 数理情報学科
講演日時
9/18(Mon) 10:15 - 10:50 (35min.)
講演題目
Type Theory with Evaluation Modalities
Title
Type Theory with Evaluation Modalities
アブストラクト
Andrew M. Pitts によって提案された Evaluation Logic は、 ``evaluation modality'' と呼ばれる様相を持つ述語論理である。彼 のもともとの体系は、直観主義論理に基づいてはいるものの、真に構 成的な解釈を与えることが難しい。この問題を解決するため、 evaluation modality と non-informative quantifier を合わせ持つ 新しい構成的型理論を提案する。
Abstract
Evaluation Logic proposed by Andrew M. Pitts is a predicate logic with modalities called ``evaluation modalities''. Though it is based on intuitionistic logic, we can hardly give a truly constructive semantics of it. To solve this problem, we propose a new constructive type theory with both evaluation modalities and non-informative quantifiers.

------------------------Session 2B(9/18(Mon)) AM: SLACS---
講演者
林 晋 (Hayashi, Susumu)
所属
神戸大学
講演日時
9/18(Mon) 11:00 - 11:35 (35min.)
講演題目
ctPX and mvPX: two extensions of PX
Title
ctPX and mvPX: two extensions of PX
アブストラクト
PX システムを
(1) ctPX: 中野の catch & throw logic
(2) mvPX: multiple value realizability
により拡張したので報告する。本研究は 小林聡, 中野浩, 石川雅一, 中崎修一 との共同研究である。
Abstract
PX system has been extended by the following features:
(1) ctPX: catch & throw logic by Nakano
(2) mvPX: multiple value realizability
These two extensions will be described. These are joint works with S. Kobayashi, H. Nakano, M. Ishikawa, S. Nakazaki.

------------------------Session 2B(9/18(Mon)) AM: SLACS---
講演者
小林 孝次郎 (Kobayashi, Kojiro)
所属
東京工業大学 情報理工学研究科 数理・計算科学専攻
講演日時
9/18(Mon) 11:45 - 12:20 (35min.)
講演題目
universal distribution の malignness を保存す る変換について
Title
Transformations that Preserve Malignness of Universal Distributions
アブストラクト
universal distribution は，確率分布に従って入 力xを与えると，どのようなアルゴリズムにおいても平均実行時間 と最悪実行時間が同じオーダーになる，という意味で，malign であ るといわれる．我々は， が malignであるための に関する条件について考える．
Abstract
A universal distribution is said to be malign in the sense that, if we give an input x with probability then, for any algorithm A the worst-case computation time and the average computation time are of the same order. We consider for which functions continue to be malign.

Session 3 ---9/18(Mon) PM: SLACS & Proof Theory Joint---

セッション３ --9月18日(月) 午後: 合同セッション--

 
 13:20 - 13:50 		 		 白旗 優 ::

     		 Strong normalization of intuitionistic set theory without equality

 13:50 - 14:00 		 		 		  break

 14:00 - 15:00 		 		 Grigori Mints 招待講演 1::

    		 
  Natural Deduction in Non-classical logic 1

 15:00 - 15:20 		 		 		  coffee break

 15:20 - 16:20 		 		 Max Kanovitch 招待講演 2::

    		 
  Linear Logic

 16:20 - 16:30 		 		 		  announcement

 18:00 - 20:00 		 		 		 懇親会 at 酔心

<< 招待講演については、別項をご参照下さい >> 。

{} アブストラクト
------------------------Session 3(9/18(Mon)) PM: SLACS & Proof Theory Joint---
講演者
白旗 優 (Shirahata, Masaru)
所属
北陸先端科学技術大学院大学
講演日時
9/18(Mon) 13:20 - 13:50 (30min.)
講演題目
Strong normalization of intuitionistic set theory without equality
Title
Strong normalization of intuitionistic set theory without equality
アブストラクト
この講演は、自然演繹に基づいた集合論システムの強標準化に関する L. ハルナスの結果を簡略化し、それをさらに発展させることを目的 とする。まず簡略化のために、自然演繹での証明図に対応する型付き ラムダ計算を導入し、それを使って強標準化定理の証明をおこなう。 また、ハルナスの証明は、集合を表す項の整序可能な集まりによって 制約されているが、そうした整序関係に依存しない場合も考えたい。
Abstract
In this talk, we will simplify and extend L. Hallnas' result on the strong normalization of the natural deduction system of set theory. We first introduce a typed lambda calculus for encoding proof figures to simplify his result. Secondly, while his result is constrained by a certain well-ordering of set terms, we will study if such a well-ordering is really necessary.

Session 4 ---9/19(Tue) AM: SLACS & Proof Theory Joint---

セッション４ --9月19日(火) 午前: 合同セッション--

 
 10:15 - 11:15 		 		 Grigori Mints 招待講演 3::

    		 
  Natural Deduction in Non-classical logic 2

 11:15 - 11:30 		 		 		  break

 11:30 - 12:30 		 		 Max Kanovitch 招待講演 4::

    		 
  Temporal Linear Logic and its Applications

 12:30 - 13:30 		 		 		  Lunch

<< 招待講演については、別項をご参照下さい >> 。

Session 5A ---9/19(Tue) PM: Proof Theory---

セッション５Ａ ---9月19日(火) 午後: Proof Theory---

 
 13:30 - 14:30 		 		 新井 紀子 ::

    		 A proper hierarchy of propositional sequent calculi

 14:30 - 15:00 		 		 		  coffee break

 15:00 - 15:50 		 		 黒田 覚 ::

    		 Feasible な２階算術について

 15:50 - 16:00 		 		 		  break

 16:00 - 16:40 		 		 上江洲 忠弘 ::

    		 無限論理和を持つ命題線形論理の無限的体系と様相論理演算子 ¥ と ？

 16:40 - 16:50 		 		 		  break

 16:50 - 17:10 		 		 鈴木 利幸 ::

    		 Encoding of QBF by MALL

{} アブストラクト
------------------------Session 5A(9/19(Tue)) PM: Proof Theory---
講演者
新井 紀子 (Arai, Noriko)
所属
広島市立大学 情報科学部
講演日時
9/19(Tue) 13:30 - 14:30 (60min.)
講演題目
A proper hierarchy of propositional sequent calculi
Title
A proper hierarchy of propositional sequent calculi
アブストラクト
命題論理体系LKでは同じ恒真式の列を証明するのにカットのある体系 に比べ カットなしの体系での方が指数関数的に証明が長くなること が知られている。また、一方ではカットを含めたLKの体系では証明を 樹状に書いても列状に書いてもその証明の長さには多項式の違いしか ないことも知られている。ここでは、カットの複雑さをその cut-formulaに含まれる論理記号の数で計って、カットなしのLKから あらゆるカットを認めた体系までのヒエラルキーを作る。多項式を比 較のベースに取ったとき、そのヒエラルキーが proper であること （ヒエラルキーが崩壊しないこと）を示す。また、カットの長さを制 限した場合、それをいかに長く設定しても、列状の証明図に比べ樹状 の証明図の方が指数関数的に長くなる例を与える。
Abstract
It is known that LK, a system of propositional sequent calculus, without a cut rule (written in tree form) does not p-simulate LK with a full cut rule (written in tree form). It is also known that LK with a full cut rule in tree-form p-simulates LK in DAG. We show that LK (in tree form) with a cut rule, where the complexity of cut formulas is bounded by (k+1) has an exponential speed-up over the one bounded by k. We also show that LK (in tree form) with a bounded complexity cut rule does not polynomially simulate cut-free LK in DAG.

------------------------Session 5A(9/19(Tue)) PM: Proof Theory---
講演者
黒田 覚 (Kuroda, Satoru)
所属
名古屋大学 人間情報学研究科 博士課程
講演日時
9/19(Tue) 15:00 - 15:50 (50min.)
講演題目
Feasible な２階算術について
Title
On feasible second order arithmetic
アブストラクト
S.Buss による Bounded Arithmetic の theory は帰納法を bounded formula に制限することによって得られるが, これにある種の内包公 理などを付け加えて得られる２階の theory がもとの theory に対し て first order conservative となることが知られている. これらの theory における各種の２階の公理の強さについてのべる.
Abstract
S.Buss introduced theories of Bounded Arithmetic by restricting induction scheme to be applied only to bounded formulae. And it is known that we obtain first order conservative extensions of such theories by adding some kind of second order schema. We will discuss about the strength of various kind of axioms in these theories.

------------------------Session 5A(9/19(Tue)) PM: Proof Theory---
講演者
上江洲 忠弘 (Uesu, Tadahiro)
所属
東京理科大学 理学部
講演日時
9/19(Tue) 16:00 - 16:40 (40min.)
講演題目
無限論理和を持つ命題線形論理の無限的体系と様相 論理演算子 ¥ と ？
Title
An infinitary system -MALL of propositional linear logic and modal operator ¥ and ？
アブストラクト
型の無限論理和を持つ命題線形論理の無限的体系 -MALL を与える。また、様相論理演算子 ¥ を持つ命題線形 論理の有限的体系 MAD¥ を与える。-MALL において を論理式Aの無限的加法的論理和 と看倣し を とする。-MALL のカット除去定理を 仲介として -MALL、MAD¥ 及び通常の命題線形論理の体系と の関係を論ずる。
Abstract
An infinitary system -MALL of propositional linear logic with -type disjunctions is introduced. Cut elimination theorem for -MALL holds. It follows from cut elimination theorem for -MALL that -MALL is a conservative extension of the ordinary finitary system of propositional linear logic, where is regarded as the formula in -MALL for each formula A.

------------------------Session 5A(9/19(Tue)) PM: Proof Theory---
講演者
鈴木 利幸 (Suzuki, Toshiyuki)
所属
弓削商船高専
講演日時
9/19(Tue) 16:50 - 17:10 (20min.)
講演題目
Encoding of QBF by MALL
Title
Encoding of QBF by MALL
アブストラクト
Abstract
Lincoln et al. shows that MALL provability is PSPACE-complete by encoding Quantified Boolean Formulas(QBF) as Multiplicative Additive Linear Logic(MALL) formulas. This encoding introduces a new propositional variable for a quantifier free matrix. We show that this artificial introduction is superfluous by a proof-theoretic argument.

Session 5B ---9/19(Tue) PM: SLACS---

セッション５Ｂ ---9月19日(火) 午後: SLACS---

 
 13:30 - 13:50 		 		 岡崎 宏光 ::

    		 初等幾何定理の大量生産

 13:50 - 14:00 		 		 		  break

 14:00 - 14:30 		 		 木下 佳樹 ::

    		 データ精製の代数

 14:30 - 15:00 		 		 		  coffee break

 15:00 - 15:30 		 		 藤田 憲悦 ::

    		 計算の直観主義的断片について

 15:30 - 15:40 		 		 		  break

 15:40 - 16:00 		 		 倉田 俊彦 ::

    		 型なし計算のモデルをなすフィルター領域について

 16:00 - 16:10 		 		 		  break

 16:10 - 16:30 		 		 Gabriel Ciobanu ::

    		 On some logical attempts in semantics of programming
	languages

 16:30 - 16:40 		 		 		  break

 16:40 - 17:10 		 		 鈴木 信行 ::

    		 Possible world semantics with graded accessibility

{} アブストラクト
------------------------Session 5B(9/19(Tue)) PM: SLACS---
講演者
岡崎 宏光 (Okazaki, Hiromitsu)
所属
熊本大学 教育学部
講演日時
9/19(Tue) 13:30 - 13:50 (20min.)
講演題目
初等幾何定理の大量生産 --- LK と NK からの推論 規則の抜粋 ---
Title
The mass production of the theorems of the elementary geometry
--- Exraction of the inference rules from LK and NK ---
アブストラクト
推論規則を LK と NK から抜粋して使い、初等幾何の定理を大量に生 産するプログラムを作ることができた。使用した推論規則は以下のも のです。三段論法、減左、& 右 (以上 LKより)、導入、 除去、& 除去 (以上 NKより)。なお 13個の幾何の公理を 使用した。
Abstract
The inference rules were extracted from LK and NK, and used to make the theorems of the elementary geometry in the computer. The program which produced them in a large quantity could be made. The used inference rules are following things: Cut, Left-Contraction, &-Right, -Introduction, -Removal. And 13 axioms of the elementary geometry were used.

------------------------Session 5B(9/19(Tue)) PM: SLACS---
講演者
木下 佳樹 (KINOSHITA, Yoshiki)
所属
電子技術総合研究所
講演日時
9/19(Tue) 14:00 - 14:30 (30min.)
講演題目
データ精製の代数
Title
An algebraic account of data refinement
アブストラクト
データ精製は, 段階的詳細化法とよばれる重要なプログラム開発手法 を説明する枠組である.
C.A.R.Hoare が1987年に書いた未刊草稿で示したデータ精製の意味を, enriched category theory によって説明する. さらに, Hoare の与 えた意味, とくに彼のいわゆる total transformation の問題点も指 摘する.
Abstract
Data refinement is a background framework for an important program development method called stepwise refinement. We give an account, using enriched category theory, for a semantics of data refinement given by C.A.R. Hoare in his 1987 unpublished manuscript. We also point out the difficulty of Hoare's semantics, especially of his "total transformation".

------------------------Session 5B(9/19(Tue)) PM: SLACS---
講演者
藤田 憲悦 (Fujita, Ken-etsu)
所属
九州工業大学 情報工学部
講演日時
9/19(Tue) 15:00 - 15:30 (30min.)
講演題目
計算の直観主義的断片について
Title
An intuitionistic fragment of -calculus
アブストラクト
計算は, Curry-Howardの原理の拡張により古典的証明に 計算的意味 を与えるために M.Parigot によって考案された複数の結 論を持つ古典的自然演繹体系である. ここでは, 計算の 直観主義的断片に を追加した体系 の以下の 証明論的性質について考察をする.
(1) NJ と の関係,
(2) の正規化証明について.
Abstract
We investigate proof theoretical property of an intuitionistic fragment of Parigot's -calculus with disjunction and conjunction (). It will be shown that conservativity of over NJ and the existence of a normal deduction in .

------------------------Session 5B(9/19(Tue)) PM: SLACS---
講演者
倉田 俊彦 (Kurata, Toshihiko)
所属
東京工業大学大学院 情報理工学研究科
講演日時
9/19(Tue) 15:40 - 16:00 (20min.)
講演題目
型なし計算のモデルをなすフィルター領 域について
Title
On filter domain construction of models for type-free -calculus
アブストラクト
交型に対してある種の順序構造(部分型関係と呼ばれる)を導入し、そ のうえで定義されるフィルター領域を用いて、型なし計算 のモデルを構成する方法が知られているが、その際すべての部分型関 係がモデルを生成するわけではない。そこで、これに対し て部分型関係がモデルを生成するための必要十分条件を与 える。
Abstract
As a way to costruct models for the type-free -calculus, filter domain construction which is realized by introducing certain pre-order (the subtype relation) over intersection types is well-known, however not any subtype relations generate -models. So, for these relations, we give a necessary and sufficient condition to induce -models.

------------------------Session 5B(9/19(Tue)) PM: SLACS---
講演者
Gabriel Ciobanu
所属
東北大学 RIEC
講演日時
9/19(Tue) 16:10 - 16:30 (20min.)
講演題目
On some logical attempts in semantics of programming languages
Title
On some logical attempts in semantics of programming languages
アブストラクト
Abstract
The talk presents some observations on the three-valued and on the four-valued logics involved in semantics of computation, namely on , , and . A relationship between and is emphasized by means of some retraction pairs. Different versions of ``and'' are connected to (different) strategies of evaluation. A deduction system for a three-valued logic is proposed.

------------------------Session 5B(9/19(Tue)) PM: SLACS---
講演者
鈴木 信行 (SUZUKI, Nobu-Yuki)
所属
茨城大学 工学部 情報工学科
講演日時
9/19(Tue) 16:40 - 17:10 (30min.)
講演題目
Possible world semantics with graded accessibility
Title
Possible world semantics with graded accessibility
アブストラクト
可能世界枠(W,R)において、「xRy」は、「yがxからアクセス可能であ ること」を意味する。現実には、y が情報源として完全には信頼しえ ない場面がある。そこで、xRy である各対(x,y) に区間 [0,1]の実数 r(x,y) を対応せしめ、これを「xからみたyの信頼度」と考えると、 新しい可能世界意味論とこれに対応する多様相論理が得られる。この 論理の形式的体系を与え、決定可能性を導く。
Abstract
In a possible world frame (W,R), `xRy' means `y is accessible from x'. In practical situations, it may happen that x cannot fully rely upon y as an information source. We attach a real number r(x,y) (in [0,1]) to each pair (x,y) with xRy as the reliability factor of y from x, and obtain a family of multimodal logics. They are characterized syntactically and proved to be decidable.

Session 6A ---9/20(Wed) AM: Proof Theory---

セッション６Ａ ---9月20日(水) 午前: Proof Theory---

 
 10:20 - 11:10 		 		 池田 一麿 ::

    		 A normal form for arithmetical derications implying the
	-consistency of arithmetic

 11:10 - 11:20 		 		 		  break

 11:20 - 11:50 		 		 鹿島 亮、山口 武志 ::

    		 On Some Decision Procedures for Implicational logics

 11:50 - 12:00 		 		 		  announcement

{} アブストラクト
------------------------Session 6A(9/20(Wed)) AM: Proof Theory---
講演者
池田 一磨 (Ikeda, Kazuma)
所属
筑波大学 数学研究科
講演日時
9/20(Wed) 10:20 - 11:10 (50min.)
講演題目
A normal form for arithmetical derivations implying the -consistency of arithmetic
Title
A normal form for arithmetical derivations implying the -consistency of arithmetic
アブストラクト
算術の証明図についての一つの標準型定理を紹介する. その定理は, までの超限帰納法によって証明される. また, それ は, 算術が -無矛盾であることを導く.
Abstract
We give a normal form theorem for arithmetical derivations. It is proved by induction up to and implies the -consistency of arithmetic.

------------------------Session 6A(9/20(Wed)) AM: Proof Theory---
講演者
鹿島 亮* (KASHIMA, Ryo),
山口 武志** (Yamaguchi, Takeshi)
所属
(*) 北陸先端科学技術大学院大学 情報科学研究科
(**)東京工業大学 情報理工学研究科
講演日時
9/20(Wed) 11:20 - 11:50 (30min.)
講演題目
On Some Decision Procedures for Implicational logics.
Title
On Some Decision Procedures for Implicational logics.
アブストラクト
文献[1]で Bunder は, いくつかの論理(直観主義, BCK, BCI, BCIW, BB'IW,他)の含意断片に対する決定手続きを与えているが, この論文 には間違いや曖昧な点があることが判明した. 本講演では, 彼のアイ デアに基づいて決定手続きを再定義し, それが直観主義論理, BCK論 理, BCI論理に対してはうまく働くことを証明する.
Abstract
In [1], Bunder introduced decision procedures for some implicational logics(intuitionistic, BCK, BCI, BCIW, BB'IW, etc.). However, this paper contains certain errors and ambiguities. In this talk, I redefine his procedures and prove the correctness of them for intuitionistic, BCK, and BCI logics.
Reference
[1] M.W.Bunder: Some Decision Procedures for Implicational Logics, Preprint, Dep. Math., Univ. Wollongong (1995).

Session 6B ---9/20(Wed) AM: SLACS---

セッション６Ｂ ---9月20日(水) 午前: SLACS---

 
 10:20 - 10:50 		 		 広川 左千夫 ::

    		 Right weakening and right contraction in LK

 10:50 - 11:00 		 		 		  break

 11:00 - 11:30 		 		 青戸 等人 ::

    		 Unique normal proof property for implicational minimal formulas

    		 in the intuitionistic logic

 11:30 - 11:50 		 		 		  announcement

{} アブストラクト
------------------------Session 6B(9/20(Wed)) AM: SLACS---
講演者
広川 左千夫 (Hirokawa, Sachio)
所属
九州大学 理学部
講演日時
9/20(Wed) 10:20 - 10:50 (30min.)
講演題目
Right weakening and right contraction in LK
Title
Right weakening and right contraction in LK
アブストラクト
Abstract
We describe a sequent calculus for classical logic, and its substructural logics determined by combinations of structural rules. It is shown that the right weakening rule and the right contraction rule can not be seperated. Moreover it is shown that if a substrucrual logic contains both, the left weakening and the left contraction are addmissible. Thus the weakening and the contraction rule have differenct feature in the left and in the right of a sequent.

------------------------Session 6B(9/20(Wed)) AM: SLACS---
講演者
青戸 等人 (Aoto, Takahito)
所属
北陸先端科学技術大学院大学
講演日時
9/20(Wed) 11:00 - 11:30 (30min.)
講演題目
Unique normal proof property for implicational minimal formulas in the intuitionistic logic
Title
Unique normal proof property for implicational minimal formulas in the intuitionistic logic
アブストラクト
直観主義論理における implicational minimal formula が NJ で一 意な -normal proofを持つための新たな十分条件を紹介する。 この条件は、以前に知られていたBCK論理での証明可能性や、深さ 2 以下という 条件を真に拡張している。
Abstract
A formula is said to have unique -normal proof property iff it has a unique -normal proof in NJ. In this talk a condition of implicational minimal formulas in the intuitionistic logic for unique -normal proof property is presented. It is shown that this condition properly includes both BCK-provability and depth 2 which are previously known conditions proved by S.Hirokawa and M.Tatsuta, respectively.