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

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)
WOLTER Frank  北陸先端科学技術大学院大学, 情報科学研究科, 助手 (20272990)
酒井 正彦  北陸先端科学技術大学院大学, 情報科学研究科, 助教授 (50215597)
Project Period (FY) 1996 – 1997
Project Status Completed (Fiscal Year 1997)
Budget Amount *help
¥2,400,000 (Direct Cost: ¥2,400,000)
Fiscal Year 1997: ¥1,300,000 (Direct Cost: ¥1,300,000)
Fiscal Year 1996: ¥1,100,000 (Direct Cost: ¥1,100,000)
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.

Report

(3 results)
  • 1997 Annual Research Report   Final Research Report Summary
  • 1996 Annual Research Report
  • Research Products

    (28 results)

All Other

All Publications (28 results)

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

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

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

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

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

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

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

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [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
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [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
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] T.Aoto and Y.Toyama: "Persistency of confluence" Journal of Universal Computer Science. Vol.3, No.11. 1134-1147 (1997)

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

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [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
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [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
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] R.Kashima: "Contraction-elimination for implicational logics" Annals of Pure and Applied Logic. Vol.84, No.1. 17-39 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] 小野寛晰: "Decidability and finite model property of substructural logics" Tbilisi Symposium on Language,Logic and Computation. (1998)

    • Related Report
      1997 Annual Research Report
  • [Publications] 成瀬博之: "A syntactic approach to Maksimova's principle of variable separation for some substructural logics" Notre Dame Journal of Formal Logic. (発表予定).

    • Related Report
      1997 Annual Research Report
  • [Publications] 青戸等人: "Persistency of confluence" Journal of Universal Computer Science. 3・11. 1134-1147 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] 青戸等人: "On composable properties of term rewriting systems" Lecture Nates in Computer Science. 1298. 114-128 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] 鹿島亮: "Contraction-elimination for implicational logics" Annals of Pure and Applied Logic. 84・1. 17-39 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] 小野寛晰: "Decidability and the finite model property of substructural logics" The Tbilisi Symposium on Language,Logic and Computation. (1997)

    • Related Report
      1996 Annual Research Report
  • [Publications] 小野寛晰: "Algebraic semantics for predicate logics and their completeness" Logic at Work. (1997)

    • Related Report
      1996 Annual Research Report
  • [Publications] バュ ステルソ: "Cut-elimination in noncommutative substructural logics" Reports on Mathematical Logic. 30. (1997)

    • Related Report
      1996 Annual Research Report
  • [Publications] 酒井正彦: "Semantics and strong sequentiality of priority term rewriting systems" Lecture Notes in Computer Sciene. 1103. 377-391 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 高橋宜孝: "条件付き項書換え系の合流性について" 電子情報通信学会論文誌. J79-D-I. 877-902 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] ヴォルターフランク: "Tense logic without tense operators" Mathematical Logic Quarterly. 145-171 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] ヴォルターフランク: "Completeness and decidability of tense logics closely related to logics above K4" Journal of Symbolic Logic. (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] ヴォルターフランク: "Properties of tense logics" Mathematical Logic Quarterly. (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 田中一之: "数学基礎論講義-不完全性定理とその発展" 日本評論社, 206 (1997)

    • Related Report
      1996 Annual Research Report

URL: 

Published: 1996-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi