• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

1997 Fiscal Year Final Research Report Summary

Applications of Mathematical Logic in Theoretical Computer Science

Research Project

Project/Area Number 08680356
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field 計算機科学
Research InstitutionJapan Advanced Institute of Science and Technology, Hokuriku

Principal Investigator

ONO Hiroakira  School of Information Science, JAIST Professor, 情報科学研究科, 教授 (90055319)

Co-Investigator(Kenkyū-buntansha) AOTO Takahito  School of Information Science, JAIST, Research Associate, 情報科学研究科, 助手 (00293390)
KASHIMA Ryo  School of Information Science, JAIST, Research Associate, 情報科学研究科, 助手 (10240756)
ISHIHARA Hajime  School of Information Science, JAIST,Associate Professor, 情報科学研究科, 助教授 (10211046)
TOYAMA Yoshihito  School of Information Science, JAIST,Professor, 情報科学研究科, 教授 (00251968)
Project Period (FY) 1996 – 1997
Keywordssubstructural logic / modal logic / term rewriting systems / constructive mathematics
Research Abstract

Main aim of this project is to study various logical problems appearing in computer science from both theoretical and practical point of view. In particular, we planned to bring the following subjects into focus, at the beginning.
1. linear logic and substructural logics, in general, as logic of action and logic of resources,
2. reasoning about knowledge, based on epistemic logic and cummulative reasoning,
3. descriptions of specifications of software based on temporal logics and their verifications,
4. reduction systems, in particular, term rewriting systems, and their applications to functional programming languages.
1. One is now developing a general theory of substructural logics without contraction rule, by using algebraic methods. The study shows that within the framework of logics without contraction rule, we can discuss various kinds of logics, including BCK logics, intuitionistic logic, Lukasiewicz's many-valued logics and even some of fuzzy logics in a uniform way. Ishihara and Kashima discussed various implicational logics and their connections with typed lambda calculi.
2. Some studies has been done by One in belief revision and its relation to reasoning of other types, like inductive reasoning and cummulative reasoning.
3. A very important theoretical study has been done by F.Wolter, who was a member of our project in 1996. Among others, he obtained strong results on the decision problems on temporal logics. This topics is related also to modal logic. Aoto and Ono have developed the study of the intuitionistic modal logics in collaboration with F.Wolter, M.Zakharyaschev and G.Bezhanishvili, who stayd at JAIST at least a half of the term of the present project.
4. Toyama and Aoto obtained interesting results on term rewriting systems, in particular on the termination, the confluence and the modularity of these systems, in collaboration with M.Sakai who was a member of our project in 1996.

  • Research Products

    (14 results)

All Other

All Publications (14 results)

  • [Publications] 小野 寛晰: "Decidability and finite model property of substauctural logics" Tbilisi Symposium on Language,Logic and Computation. (1998)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 成瀬 博之: "A syntactic approach to Maksimra's principle of variable separationfor some substructural logics" Notre Dame Journal of Formal Logic. 発表予定.

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 青戸 等人: "Persistency of confluence" Journal of Universal Computer Science. 3・11. 1134-1147 (1997)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 青戸 等人: "On composable properties of term rewriting systems" Lecture Notes in Computer Science. 1298. 114-128 (1997)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 石原 哉: "Sequential continuity of linear on appings in constructive mathematics" Journal of Universal Computer Science. 3・11. 1250-1254 (1997)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 鹿島 亮: "Contraction-elimination for implicational logics" Annals of Pure and Applied Logic. 84・1. 17-39 (1997)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] H.Ono: "Decidability and finite model property of substructural logics" The Tbilisi Symposium on Language, Logic and Computation. CSLI Lecture Mote. (1998)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] M.Sakai and Y.Toyama: "Semantics and strong sequentiality of priority term rewriting systems" Proc.of the 7th International Conference on Rewriting Techniques and Applications, Lecture Notes in Comput.Sci.1103. Springer-Verlag. 377-391 (1996)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] T.Aoto and Y.Toyama: "On composable properties of term rewriting systesms" Proc.of the 6th International Conference on Algebraic and Logic Programming (ALP'97), Lecture Notes in Cpmput.Sci.1298. Springer-Verlag. 114-128 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] T.Aoto and Y.Toyama: "Persistency of confluence" Journal of Universal Computer Science. Vol.3, No.11. 1134-1147 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] H,Ishihara: "Sequential continuity of linear mappings in constructive mathematics" Journal of Universal Computer Science. Vol.3, No.11. 1250-1254 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] H.Ishihara: "Effectiveness of the completeness theorem for an intermedicate logic" Journal of Universal Computer Science. Vol.3, No.11. 1255-1265 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] R.Kashima and T.Yamaguchi: "On the difficulty of writing out formal proofs in arithmetic" Mathematical Logic Quarterly. Vol.43. 328-332 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] R.Kashima: "Contraction-elimination for implicational logics" Annals of Pure and Applied Logic. Vol.84, No.1. 17-39 (1997)

    • Description
      「研究成果報告書概要(欧文)」より

URL: 

Published: 1999-03-16  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi