\documentclass[a4j,11pt]{jarticle}
\usepackage{prkintou}
%\setlength{\textwidth}{160pt}
%\renewcommand{\baselinestretch}{2}
%\pagestyle{empty}
\begin{document}
\pagenumbering{roman}
\thispagestyle{empty}
\begin{center}
{\Huge
部 分 構 造 論 理 の 研 究
}
\\[10mm]
{\Large
( 研究課題番号 \ \ \ 10640103 )
}
\\[10mm]
平成10年度 $\sim$ 平成11年度科学研究費補助金 (基盤研究(C)(2)) \\
研究成果報告書
\\[80mm]
{\Large
平成12年4月
}
\\[30mm]
研 究 代 表 者\ \ \ {\Large 古\ \ 森\ \ 雄\ \ 一}
\\[2mm]
( 千葉大学 \ \ 理学部 \ \ \ 教授 )
\end{center}
\newpage
\begin{center}
{\Large
はしがき
}
\\[10mm]
\end{center}
本研究は, 「部分構造論理の研究」の表題のもとに, 平成10年度から平成11年度
にかけての二年間にわたり, 文部省科学研究費補助金の交付を受けて行われた。
本研究の目的は,	カテゴリー文法, relevant 論理, BCK 論理, 線形論理などの部
分構造論理の性質を明らかにすることであった。
この「はしがき」の末尾の「研究発表」にあるように, 研究分担者たちの活発
な研究活動により, 部分構造論理の性質は明らかになりつつある。
ここでは, 研究代表者の古森による２つの成果について述べる。

第一のものは $P-W$ 問題のラムダ計算による解決である。これはもともと,
永山操の $P-W$ 問題の Genzten 流体系による研究とほぼ同時期に, 廣川により
始められたものである。永山の方法で 1993 年の夏に永山と古森は
$P-W$ 問題を解決するが, 廣川の方法では上手くいかなかった。
古森は 1994 年 12 月 5 日の NSL'94 (Workshop on Non-standard Logic and
Logical Aspects of Computer Science (金沢)) の講演で, 廣川の方法に
永山の方法を取り入れれば容易にラムダ計算による解決が得られるとの見解
を述べた。廣川はそれを実行したが, 古森が思っていたほど簡単ではなかった。
しかし, 廣川は根気よく研究を続けラムダ計算による解決をほぼ達成した。
最終的には, 永山が証明の吟味をして論文にまとめた。

第二のものは鹿島亮による古典論理の自然演繹の体系を古森が少し変えた体系
についてのものである。この体系についての現在までの最もよい結果は, 鹿島に
よる「与えられた任意の証明図を部分論理式特性をもつ証明図に変形すること
ができる」というものである。唯一の結論を持つ古典論理の自然演繹の体系で
正規形が部分論理式特性を持つというものは知られていなかったので, この結果は
そのような最初の体系を示したことになる。しかし, この変形規則は Church-Rosser
性を持っていない。この体系の望ましい性質を保ったまま Church-Rosser 性を持つ
ように変形規則を作り上げることと, その変形規則の計算規則としての
意味(Catch/Throw メカニズムとの関連など)を明らかにすることは非常に興味深い
残された研究課題である。

なお, 本報告書の内容は全て\\
http://www.math.s.chiba-u.ac.jp/\~{ }komori/kaken99/\\
で見ることができる。本報告書に収めることができなかった論文
の幾つかも上記 URL (uniform resourse locator) から入手可能である。\\[5mm]
\begin{flushright}
2000 年 4 月 10 日\\
古森 雄一
\end{flushright}
%\vspace{2cm}
\newpage
\noindent
{\Large 研究組織}\\[5mm]
\begin{tabular}{cll}
研究代表者 & 古森 雄一 & (千葉大学 理学部 教授)\\[2mm]
研究分担者 & 中村 吉邑 & (千葉大学 理学部 教授)\\
研究分担者 & 辻 尚史   & (千葉大学 理学部 教授)\\
研究分担者 & 桜井 貴文 & (千葉大学 理学部 助教授)\\
研究分担者 & 山本 光晴 & (千葉大学 理学部 助手)\\
研究分担者 & 金沢 誠   & (千葉大学 文学部 助教授)\\
研究分担者 & 廣川 佐千男 & (九州大学 大型計算機センター 教授)\\
研究分担者 & 藤田 憲悦 & (九州工業大学 情報工学部 講師)\\[2mm]
研究協力者 & 杉山健一  & (千葉大学 理学部 助教授)
\end{tabular}
\ \\[10mm]
{\Large 研究経費}\\[5mm]
\begin{tabular}{cr}
平成10年度 & \hspace{10mm} 2,200千円\\
平成11年度 & \hspace{10mm} 1,600千円\\
& \\
    計     &3,800千円
\end{tabular}
\ \\[10mm]
{\Large 研究発表}\\[5mm]
\ \ {\large (1)学会誌等}
\begin{list}{}{}
\item
Sachio Hirokawa, Yuichi Komori and  Misao Nagayama,
A lambda proof of the $P-W$ theorem, 
The Journal of Symbolic Logic ( to appear )
\item
Masahiko Sato, Takafumi Sakurai, Rod Burstall,
Explicit Environments,
in Proceedings of Fourth International Conference
on Typed Lambda Calculus and its Application (TLCA '99),
LNCS 1581, pp. 340 -- 354, 1999
\item
Takafumi Sakurai,
Categorical Model Construction for Proving Syntactic Properties,
International Journal of Foundations of Computer Science,
to appear
\item
Takafumi Sakurai,
Categorical Model Construction for Proving Syntactic Properties,
in Proceedings of Third Fuji International Symposium
on Functional and Logic Programming (eds. M. Sato and Y. Toyama),
World Scientific,
pp. 187 -- 206, 1998
\item
Mitsuharu Yamamoto and Masami Hagiya,
Evolution of Inductive Definitions,
IWPSE99: International Workshop on Principles of Software Evolution,
17--21, 1999
\item
山本 光晴, 高橋 孝一, 萩谷 昌己, 西崎 真也, 玉井 哲雄,
グラフ探索アルゴリズムの形式的検証とモデル検査への応用について,
数理解析研究所講究録1125, 129--141, 2000
\item
山本 光晴, 高橋 孝一, 萩谷 昌己,
モデル検査アルゴリズムの検証について,
日本ソフトウェア科学会第16回大会論文集, 1999
\item 
Makoto Kanazawa  Lambek calculus: Recognizing power and
      complexity.  In JFAK. Essays Dedicated to Johan van Benthem on
	   the Occasion of his 50th Birthday 
	   (Jelle Gerbrandy, Maarten Marx, Maarten
	    de Rijke, and Yde Venema, editors),\\
      http://turing.wins.uva.nl/~j50/cdrom/
%	   Vossiuspers, <a href="http://www.aup.nl">
      Amsterdam University Press, 1999
\item
佐塚秀人, 長野大介, 廣川佐千男, 
証明とモデルを生成するインターネットプルーバー,
九州大学大型計算機センター計算機科学研究報告 16, 1--6, 1999
\item
Keiichi Mishima, Naoyuki Kato and Sachio Hirokawa, 
GUI for Geometric Inference Engine on Internet,
Proceedings of Webnet'99, 1360--1361, 1999
\item
K.Fujita,
Explicitly Typed $\lambda\mu$-Calculus for Polymorphism and Call-by-Value,
Lecture Notes in Computer Science (Springer) Vol.1581, pp.162--176, 1999,
Typed Lambda Calculi and Applications (TLCA '99)
\item
K.Fujita, 
A Binary-Conclusion Natural Deduction System,\\
Logic Journal of the Interest Group in Pure and Applied Logics
(Oxford University Press), Vol. 7, No. 4, pp.517--545, 1999
\item
K.Fujita,
Domain-Free $\lambda\mu$-Calculus for Polymorphism and Call-by-Value,
京都大学数理解析研究所講究録 Vol.1106, pp.37--49, 1999
\item
K.Fujita,
Multiple-Conclusion System as Communication Calculus,
Electronic Notes in Theoretical Computer Science (Elsevier Science),
Vol. 31, No. 1, pp. 167--182, 2000, 
Computing: the Australasian Theory Symposium 2000
\item
藤田 憲悦, 
部分型推論の困難さに関する一考察,
コンピュータソフトウェア, Vol.17, No.2, 2000 (予定)
\item
K.Fujita,
{\em On Proof Terms and Embeddings of Classical Substructural Logics},
Studia Logica (Kluwer Academic),
An International Journal for Symbolic Logic, Vol.61, No.2, pp.199-221, 1998
\item
K.Fujita,
Calculus of Classical Proofs II,
Transactions of Information Processing Society of Japan (情報処理学会論文誌), 
Vol. 39, No.12, 
pp. 3269--3281, 1998
\item
K.Fujita,
Polymorphic Call-by-Value Calculus based on Classical Proofs,
Lecture Notes in Artificial Intelligence (Springer) Vol.1476, pp.170-182, 
1998, 
Artificial Intelligence and Symbolic Computation 
Theory, Implementations and Applications (AISC '98)
\item
K.Fujita,
Type Inference for Domain-Free $\lambda 2$,
Technical Reports in Computer Science and Systems Engineering,
CSSE--5, Kyushu Institute of Technology, July, 1999
\item
K.Fujita,
A sequent-conclusion natural deduction system with bounded length,
Proceedings of The Third Symposium on Algebra, Languages and Computation
 -- 1999 JAMS Annual Meeting --  (Ed. Teruo Imaoka),  1--11, 
Osaka University, 1999
\item
K.Fujita,
Multiple-Conclusion System as Communication Calculus,
Electronic Notes in Theoretical Computer Science (Elsevier Science),
Vol. 31, No. 1, pp. 167--182, 2000, 
Computing: the Australasian Theory Symposium 2000 \\
(* http://www.elsevier.nl/locate/entcs/volume31.html *)
\item
K. Fujita and S. Obara,
Safe Dynamics for Distributed Programming,
Technical Reports in Computer Science and Systems Engineering
CSSE--8, Kyushu Institute of Technology, March, 2000
\item
藤田憲悦, 小原誠一,
分散プログラミングのための安全な動的型, 
情報処理学会九州支部研究会 3C--5, 362--369, 2000
\end{list}
%----------------------------------------------------------------------
\ \ \ {\large (2)口頭発表}
\begin{list}{}{}
\item
古森 雄一,
A Natural Deduction for Classical Logic, in which there exists a proof
with the  Subformula Property,
MLG 研究集会(越後湯沢),
2000年1月10日
\item
金沢 誠, 
Developments in Learnability Theory, 
Third International Conference on Information-Theoretic
          Approaches to Logic, Language, and Computation.  Hsi-Tou,
          Taiwan,
1998年6月16日
\item
金沢 誠, 
Learning Categorial Grammars: Identification in the Limit
          and Parameter Setting, 
Logical Aspects of Computational Linguistics.  Grenoble,
          France,
1998年12月15日
\item
金沢 誠, 
Algorithmic Learning of Grammars and the Language
          Acquisition Device, 
11th International Congress of Logic, Methodology and
          Philosophy of Science.  Krakow, Poland, 
1999年8月22日
\item
廣川佐千男, WWW上の幾何推論システム,
人工知能学会 人工知能基礎論研究会 資料 SIG-FAI-9801,
1998年5月28日
%\item
%馬場 謙介, 古典論理の並行計算, 
%Proof Animationセミナー, 
%平成10年7月3日
\item
廣川佐千男, Classical Formulas as Types of Lambda-Nu-Calculus,
Logic Colloquium'98,
1999年8月9日
%\item
%馬場謙介, Parallel Reduction in lambda-mu-calculus,
%SLACS98, 
%平成10年10月14日
%\item
%佐塚秀人, 証明とモデルを生成するインターネットプルーバー,
%第16回九州大学大型計算機センター計算機科学研究集会,
%平成10年11月20日
%\item
%三島圭一, GUI for Geometric Inference Engine on Internet,
%Webnet'99, 
%平成10年11月20日
%\item
%三島圭一, インターネット上初等幾何推論システムのGUI,
%organization="情報処理学会九州支部研究会 4C-5",
%平成11年3月16日
%\item
%馬場健介, Parallel Reduction in lambda-mu-calculus,
%7th Asian Logic Conference,
%平成11年6月9日
\item
廣川佐千男,
クリプケモデル生成とJavaアプレットとしての実現
第13回人工知能学会全国大会,
1999年6月16日
\item
廣川 佐千男,
初等幾何推論の多面的表示方式,
第13回人工知能学会全国大会,
1999年6月16日
\item
藤田 憲悦,
Multiple-conclusion system as communication calculus,
Computing: the Australasian Theory Symposium (CATS 2000),
2000年2月1日
\item
杉山健一, On zeta functions of smooth manifolds and elliptic cohomology,
多変数解析セミナー, 1999年7月
\item
杉山健一, Hodge あるいは Tate 予想の成立する例の構成
          (Heisenberg 代数の表現論の観点から),
金沢大学数学談話会, 2000年3月
\end{list}
%------------------------------------------------------------------
\newpage
{\Large   目次}
\\[5mm]
\begin{tabular}{lrr}
モデル検査アルゴリズムの検証について   & $\dots$ & 1 \\
\ \ \ \ \ \  山本 光晴  他著           &   & \\
% P4
証明とモデルを生成するインターネットプルーバー & $\dots$ & 5 \\
\ \ \ \ \ \  廣川佐千男 他著           &   & \\
% P6
A lambda proof of the $P-W$ theorem   & $\dots$    & 11 \\
\ \ \ \ \ \  Sachio Hirokawa, Yuichi Komori et al.  &  & \\
% P14
A Natural Deduction for Classical Logic, in which there exists a proof & &\\
with the  Subformula Property & $\dots$ &  25\\
\ \ \ \ \ \  Yuichi Komori    &  & \\
% P4
Lambek Calculus: Recognizing Power and Complexity & $\dots$ & 29 \\
\ \ \ \ \ \   Makoto Kanazawa & & \\
% P14
Infiniteness of Proof($\alpha$) is Polynomial-Space Complete 
& $\cdots$ & 43 \\
\ \ \ \ \ \  Sachio Hirokawa & & \\
% P10
GUI for Geometric Inference Engine on Internet & $\dots$ & 53 \\
\ \ \ \ \ \  Sachio Hirokawa et al. & & \\
% P2
A Binary-Conclusion Natural Deduction System & $\dots$ & 55 \\
\ \ \ \ \ \  Ken-etsu Fujita & & \\
% P30
Multiple-Conclusion System as Communication Calculus & $\dots$ & 85 \\
\ \ \ \ \ \ Ken-etsu Fujita & & \\
% P16
\end{tabular}
\end{document}
