\documentclass{article}
\oddsidemargin 0cm \evensidemargin 0cm
\topmargin 0.46cm \headheight 0cm \headsep 0cm
\textheight 23cm \textwidth 16cm
\pagestyle{empty}
\newcommand{\Item}{\par\noindent}
\newcommand{\Bibitem}{\par\smallskip\noindent}

\begin{document}

\noindent(�ʎ��l��14)

\begin{quote}\large
ABASTRACTS OF RESEARCH PROJECT GRANT-IN-AID\\
FOR SCIENTIFIC RESEARCH (1999)
\end{quote}

\Item 1. RESEARCH INSTITUTION NUMBER: 12501

\Item 2. RESEARCH INSTITUTION: Chiba University

\Item 3. CATEGORY: Grant-in-Aid for Scientific Research (C)(2)

\Item 4. TERM OF PROJECT: (1998 $\sim$ 1999)

\Item 5. PROJECT NUMBER: 10640103

\Item 6. TITLE OF PROJECT: A Study of Substractural Logics

\Item 7. HEAD INVESTIGATOR\\
\begin{tabular}{p{1em}p{4em}p{10em}p{9em}p{10em}p{5em}}
  & 10022302 & Komori, Yuichi &
  Chiba University & Faculty of Science &
  Professor
\end{tabular}

\Item 8. INVESTIGATORS\\
\begin{tabular}{p{1em}p{4em}p{10em}p{9em}p{10em}p{5em}}
(1) & 60183373 & Sakurai, Takafumi &
  Chiba University & Faculty of Science &
  Assistant Professor \\
(2) & 00291295 & Yamamoto, Mitsuharu &
  Chiba University & Faculty of Science &
  Research Associate \\
(3) & 20261886 & Kanazawa, Makoto &
  Chiba University & Faculty of Letters &
  Assistant Professor \\
(4) & 40126785 & Hirokawa, Sachio &
  Kyushu University & Computer Center &
  Professor \\
(5) & 30228994 & Fujita, Ken-etsu &
   Kyushu Institute of Technology & Faculty of Informatic Technology &
  Lecturer \\
\end{tabular}

\Item 9. SUMMARY OF RESEARCH RESULTS
 \begin{enumerate}
   \item Recently lambda calculus unites studies of substructural logics,
    	the intutionistic logic and the classical logic.
		In this context, Kashima has posed a Natural deduction system for the
	 	classical implicational logic. His system has three rules, the
	  	elimination of
		the implication, the introduction of the implication and the case rule.
		Komori has noticed that the introduction of the implication is
		derivable from the case rule and the weakening. So we have gotten
		the system $TA_\mu$ from Kashima's system by replacing the introduction
		of implication by the weakening.
		While the type assignment system $TA_\lambda$
		gives a natural deduction for implicational intuitionistic logic,
		the type assignment system $TA_\mu$ gives a natural deduction for
		classical implicational logic.
		Moreover for any classical implicational theorem $\alpha$ there exists
		a proof of $\alpha$ in $TA_\mu$ enjoying the subformula property.
		Still more $\lambda$--calculus can be simulated in $\mu$--calculus.
	\item A new system of calculus comes out of the above result.
		We are investigating the meaning of the new calculus.
	\item Fujita has actively studied on multiple-conclusion natural
		deduction system and $\lambda\mu$-calculus, and then has written
		many papers.
%
	\item The problem on the decidablity of BB'IW logic is one of the most
		difficult mathematical problem. We are wrestling with the problem.
	\item	Kanazawa has investigated Categorial Grammars and has gotten
		excellent results.
	\item Sakurai has investigated Categorical model of lambda-calculus and
		has written two good papers.
	\end{enumerate}

\vfill
\Item 10. KEY WORDS\\
\begin{tabular}{p{12em}p{12em}p{12em}}
(1) Substructural Logic & (2) Classical Logic & (3) Intuitionistic Logic \\
(4) BCK Logic & (5) Lambda Calculus & (6) Type Theory
\end{tabular}

\begin{center}
(CONTINUE TO NEXT PAGE)
\end{center}

\newpage
\Item 11. REFERENCES

\Bibitem
Sachio Hirokawa,
{A lambda proof of the $P-W$ theorem},
{\em The Journal of Symbolic Logic},
To appear.

\Bibitem
Takafumi Sakurai,
{Categorical Model Construction for Proving Syntactic Properties},
{\em Int. Journal of Foundations of Computer Science},
To appear.

\Bibitem
Makoto Kanazawa,
{Lambek calculus: Recognizing power and complexity},
{\em In Essays 
      Dedicated to Johan van Benthem on the Occasion of his 50th
      Birthday}, (cf. http://turing.wins.uva.nl/~j50/cdrom/) 1999.

\Bibitem
Ken-etsu Fujita,
{Explicitly Typed $\lambda\mu$-Calculus for Polymorphism and Call-by-Value},
{\em Typed Lambda Calculi and Applications (TLCA '99)},
LNCS 1581, pages 162--176, 1999.

\Bibitem
Ken-etsu Fujita,
{Multiple-Conclusion System as Communication Calculus},
{\em Electronic Notes in Theoretical Computer Science (Elsevier Science)},
Vol. 31, No. 1, pages 167--182, 2000.

\Bibitem
Keiichi Mishima,
{GUI for Geometric Inference Engine on Internet},
{\em Proceedings of Webnet'99},
pages 187--206, 1999.

\end{document}
