JAMS '98 Annual Meeting プログラム

日時:平成10年8月4日〜8月6日

場所:大阪大学コンベンションセンター

◎分科会番号 1 形式体系と計算(Formal systems and computation)

代表者氏名 八杉満利子

  4日午後13:-17:, 5日午前9:30-12:30 

  (OHP・白板、PC画面を写すプロジェクタ)

8月4日(火曜日) 

1. 13:00 - 14:30  多項式時間計算可能数学について(竹内泉・京都大)

2. 14:45 - 16:15  部分構造論理について(小野寛晰・北陸先端大)

3. 16:30 - 17:00  (林晋・神戸大)-前半

8月5日(水曜日) 

4. 9:45 - 10:45 (林E晋・神戸大)-後半

5. 11:00 - 12:30  線形論理に基づいた論理型言語について(田村直之・神戸大)

----------------------------------

講演アブストラクトおよび連絡先

研究代表者 八杉満利子・京都産大

      yasugi@cc.kyoto-su.ac.jp

1. 多項式時間計算可能数学について(竹内泉・京都大)

takeuti@kuis.kyoto-u.ac.jp

 数学の諸概念について計算可能性の立場から見直した、計算可能

数学が最近注目されている。それに対し、単なる計算可能性ではな

く、計算時間を限定を施した多項式時間計算可能数学が考えられる。

本発表では、多項式時間計算可能数学と構成主義数学との関係につ

いて紹介する。また、多項式時間計算可能函数よりも少し小さいK

という函数の範疇に関するK計算可能性についても触れる。

2. 部分構造論理について(小野寛晰・北陸先端大)

  ono@jaist.ac.jp

 まず部分構造論理の研究を概説し、つぎに小野が現在関心を持っている

いくつかのトピックスについてふれる。とくに、最近得られた

証明論的方法に基く結果と、代数的手法を用いて得られた結果を紹介する。

古典論理や直観主義論理は Gentzen 流の sequent 計算により

形式化することができる。sequent 計算における証明は、基本的な

sequent ( initial sequent )に、各論理記号に対する推論規則、

cut 規則および構造規則を繰り返し適用することにより得られる。

このうち構造規則はどちらかといえば補助的な規則とみなされてきた。

ところが最近になり、これまでその研究の動機が異なるために

独自な立場からそれぞれ研究されてきたさまざまな非古典論理は、

形式的には古典論理や直観主義論理からいくつかの構造規則を

とり除いた体系とみなせることがわかってきた。表題の部分構造

論理とはこのようなタイプの非古典論理に対する総称である。

そして部分構造論理の研究は、異なった背景を持ついろいろな

部分構造論理を統一的な立場から論じていくことを目指している。

このようなアプローチにより、これまであるタイプの論理に個有

なものと思われてきた論理的性質がなにに由来しているのかを

明らかにすることが可能になる。たとえば、構造規則の一つである

縮約( contraction )規則を持つ論理は、述語論理の多くの場合に

決定不能になり、また命題論理であればたとえ決定可能であっても

その決定手続きの計算量が非常に大きくなることがわかる。

部分構造論理の例としては、線形論理や適切含意の論理、また

カテゴリ文法の基礎づけをあたえる Lambek 計算、BCK 論理など

がある。また Lukasiewicz の多値論理は BCK 論理の拡張体系とし

て位置づけられる。また最近になり、論理体系としてのファジー

論理は、このような枠組の中で考えることにより、より明確な理解を

得ることができることがわかってきた。

3. 証明アニメーション(林晋・神戸大学)

hayashi@pascal.seg.kobe-u.ac.jp

 Proof Animation とは Curry-Howard の原理により証明をテストしデバッグ

する方法である。本講演では、Proof Animation Project の経緯と計画について

述べ、 その最初の支援系 prototype である ProofWorks を紹介する。

また、Curry-Howard の対応にもとづく、Proof Engineering (形式的証明構築の

工学)の可能性についても言及する。

4. 線形論理に基づいた論理型言語について(田村直之・神戸大)

tamura@kobe-u.ac.jp

1. Uniform proof (by D. Miller) と 論理型言語

2. 線形論理の概要

3. 線形論理での Uniform proof (by J. Hodas & D. Miller)

4. 線形論理型言語 Lolli (by J. Hodas & D. Miller)

5. IO-model (by J. Hodas & D. Miller)

6. Leveled IO-model

7. Lolliのコンパイラ処理系 LLP

8. 関連研究の紹介 (LO, Lygon, Forum, HACL)

9. LLPのデモンストレーション

(PC画面を映すプロジェクタが使える場合)



../
/
Last modified: Wed Jul 1 16:27:48 JST 1998