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

Studies on logical structures of arithmetic and computation

Research Project

Project/Area Number 09440072
Research Category

Grant-in-Aid for Scientific Research (B)

Allocation TypeSingle-year Grants
Section一般
Research Field General mathematics (including Probability theory/Statistical mathematics)
Research InstitutionTOHOKU UNIVERSITY

Principal Investigator

TANAKA Kazuyuki  Grad. School of Science, Tohoku Univ., Prof., 大学院・理学研究科, 教授 (70188291)

Co-Investigator(Kenkyū-buntansha) KASHIMA Ryo  Grad. Sc. of Info. Sci. and Eng., Tokyo Inst. Tech., Lec., 大学院・情報理工学研究科, 講師 (10240756)
HORAI Masako  Grad. Sc. of Info. Sci. and Eng., Tokyo Inst. Tech., Prof., 大学院・情報理工学研究科, 教授 (00015588)
AKAMA Yohji  Grad. School of Science, Tohoku Univ., Assoc. Prof., 大学院・理学研究科, 助教授 (30272454)
HASEGAWA Ryu  Grad. School of Math. Sci., Univ. of Tokyo, Assoc. Prof, 大学院・数理科学研究科, 助教授 (20243107)
TATSUTA Makoto  Grad. School of Science, Kyoto Univ., Assoc. Prof, 大学院・理学研究科, 助教授 (80216994)
廣川 佐千男  九州大学, 大型計算機センター, 教授 (40126785)
安本 雅洋  名古屋大学, 大学院・多元数理科学研究科, 助教授 (10144114)
菊池 誠  神戸大学, 大学院・自然科学研究科, 助手 (60273801)
Project Period (FY) 1997 – 1999
Project Status Completed (Fiscal Year 1999)
Budget Amount *help
¥13,900,000 (Direct Cost: ¥13,900,000)
Fiscal Year 1999: ¥3,800,000 (Direct Cost: ¥3,800,000)
Fiscal Year 1998: ¥4,200,000 (Direct Cost: ¥4,200,000)
Fiscal Year 1997: ¥5,900,000 (Direct Cost: ¥5,900,000)
Keywordslogical structures / theory of computation / type theory / formal arithmetic / second order arithmetic / reverse mathematics / bounded arithmetic / lambda calculus / ロジック / 証明論 / 算術のモデル / 数学基礎論
Research Abstract

K. Tanaka studied along the program of reverse mathematics how much of set theory is needed to prove a theorem of ordinary mathematics. By observing properties of countable models of WKL_0, he proved (jointly with T. Yamazaki and S. Simpson) new conservation results of WKL_0 over RCA_0. Y. Akama introduced an intersection typing system for combinatory logic, and showed that it is sound and complete for the class of partial combinatory algebras. M. Horai has shown that the Curry-Howard isomorphism between higher-order intuitionistic logic and calculus of constructions can be better formulated when a modified version of higher-order type theory is introduced. She also studied the lambda-representability of functions over free structures with respect to the simple type system, as well as the notion of recursive functions over free-structures. M. Tatsuta investigated realizability interpretations of monotone coinductive definition. He proved, among others, that full monotone coinductive definitions are not sound while restricted ones are. R. Hasegawa studied applications of analytic functions to theoretical computer science. R. Kashima obtained several important results on relevant logic.

Report

(4 results)
  • 1999 Annual Research Report   Final Research Report Summary
  • 1998 Annual Research Report
  • 1997 Annual Research Report
  • Research Products

    (40 results)

All Other

All Publications (40 results)

  • [Publications] Y.Akama: "SN combinators and partial combinatory algebras"Lec.Notes in Comp.Science. 1379. 302-316 (1998)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] R.Hasegawa: "An Analysis of divisibility orderings and reaursive path orderings"Lec.Notes in Comp.Science. 1345. 283-296 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] R.Kashima and N.Kamide: "Substructural implicational logics including the relevant logic E"Studia Logica. 63. 181-212 (1999)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] M.(Horai)Takahashi: "Lambda-representable functions over term algelras"Int.J.of Foundations of Comp.Sci.. (印刷中). (2000)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] K.Tanaka and T.Yamazaki: "A non-standard constrnetion of Haar measare and WKLO"Journal of Symbolic Logic. (印刷中). (2000)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] M.Tatsuta: "Realizability of monotone conductive definitions and its application to program synthesis"Lec.Notes in Comp.Science. 1422. 338-364 (1998)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] 田中一之(編): "数学の基礎をめぐる論争"シュプリンガー・フェアラーク東京. 224 (1999)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] 森田康夫: "整数論"東京大学出版会. 284 (1999)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] Y. Akama: "SN combinators and partial combinatory algebras"Lecture Notes in Computer Science. 1379. 302-316 (1998)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] R. Hasegawa: "An analysis of divisibility orderings and recursive path orderings"Lecture Notes in Computer Science. 1345. 283-296 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] R. Kashima and N. Kamide: "Substructural implicational logics including the relevant logic E"Studia Logica. 63. 181-212 (1999)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] S. Hirokawa, Y. Komori and M. Nagayama: "A lambda proof of the P-W theorem"Journal of Symbolic Logic. (to appear).

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] M. (Horai) Takahashi: "Lambda-representable functions over term algebras"Int. J. of Foundations of Computer Science. (to appear).

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] K. Tanaka and T. Yamazaki: "A non-standard construction of Haar measure and WKLo"Journal of Symbolic Logic. (to appear).

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] M. Tatsuta: "Realizability of monotone coinductive definitions and its application to program synthesis"Lecture Notes in Computer Science. 1422. 338-364 (1998)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] T. Yamazaki: "Some more conservation results on the Baire category theorem"Mathematical Logic Quarterly. 46. ((to appear)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] 田中 一之、山崎 武: "2階算術と有界選択公理"京大数理解析研 講究録. 1096. 84-88 (1999)

    • Related Report
      1999 Annual Research Report
  • [Publications] M.Takahashi: "Lambda-representable functions over term algebras"J.Foundations of Computer Science. 印刷中. (2000)

    • Related Report
      1999 Annual Research Report
  • [Publications] S.Hirokawa,Y.Komori,M.Nagayama: "An application of simply eyped λ-calculus to relevance logic P-W"J.Symbolic Logic. 印刷中. (2000)

    • Related Report
      1999 Annual Research Report
  • [Publications] R.Kashima,N.Kamide: "Substructural implicational logic including the relevant logic E"Studia Logica. 63. 181-212 (1999)

    • Related Report
      1999 Annual Research Report
  • [Publications] M.Tatsuta: "Uniqueness of D-normal proofs"Proc. Of 7th Asian Logic Conf.. 41-42 (1999)

    • Related Report
      1999 Annual Research Report
  • [Publications] T.Yamazaki: "Some move conservation results on the Baire category theorem"Mathematical Logic Quarterly. 印刷中. (2000)

    • Related Report
      1999 Annual Research Report
  • [Publications] 田中一之(編): "数学の基礎をめぐる論争"シュプリンガー フェアラーク東京. 24 (1999)

    • Related Report
      1999 Annual Research Report
  • [Publications] 森田康夫: "整数論"東京大学出版会. 284 (1999)

    • Related Report
      1999 Annual Research Report
  • [Publications] K.Tanaka,T.Yamazaki: "A non-standard construction of Haar measure and WKLo" Journal of Symbolic Logic. (印刷中). (1999)

    • Related Report
      1998 Annual Research Report
  • [Publications] M.Takahashi: "Lambda-representable functions over free structures revisited" Proc.of 3rd Fuji Int.Symp.on Func.and Logic Programming. 1-19 (1998)

    • Related Report
      1998 Annual Research Report
  • [Publications] G.Takeuti,M.Yasumoto: "Forcing on Bounded Avithmetic II" Journal of Symbolic Logic. 63. 860-868 (1998)

    • Related Report
      1998 Annual Research Report
  • [Publications] S.Hirokawa: "Infiniteness of proof(alpha)is polynomial-space complete" Theoretical Computer Science. 206・1-2. 331-339 (1998)

    • Related Report
      1998 Annual Research Report
  • [Publications] M.Tatsuta: "Realizability for Constractive Theory of Functions and Classes and Its Application to progranc Synthesis" Proc.of 13th Ann.IEEE Symp.Logic in CS. 358-367 (1998)

    • Related Report
      1998 Annual Research Report
  • [Publications] R.Kashima,N.Kamide: "Substructural implicational logic includiog the relevant logic E" Studia Loyica. (印刷中). (1999)

    • Related Report
      1998 Annual Research Report
  • [Publications] M.Takahashi,M.Dezani,M.Okada: "Theories of Types and Proofs" 日本数学会(MSJ-Memoirs Vol.2), 295 (1998)

    • Related Report
      1998 Annual Research Report
  • [Publications] 田中 一之: "数学の基礎をめぐる論争" シュプリンガー フェアラーク東京, 224 (1999)

    • Related Report
      1998 Annual Research Report
  • [Publications] K.Tanaka and T.Yamazaki: "A non-standard construction of Haar measure and weak Konig's Iemma" Journal of Symbolic Logic. (発表予定).

    • Related Report
      1997 Annual Research Report
  • [Publications] R.Hasegawa: "An analysis of divisibility orderings and recursive path orderings" Lec.Notes in Comp.Sci.1345. 283-296 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] M.Tatsuta: "Realizability for conseructive theory of functions and classes and its application to program synthesis" Lec.Notes in Comp.Sci.(発表予定).

    • Related Report
      1997 Annual Research Report
  • [Publications] G.Takeuti and M.Yasumoto: "Forcing on bounded arithmetic" Journal of Symbolic Logic. (発表予定).

    • Related Report
      1997 Annual Research Report
  • [Publications] R.Kashima: "Contraction-elimination for implicational logics" Ann.Pure and Applied Logic. 84. 17-39 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] M.Kikuchi: "Kolmogoror complexity and the second incompleteness theorem" Archive for Math.Logic. 36. 437-443 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] 田中一之: "逆数学と2階算術" 河合文化教育研究所, 118 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] 吉野崇, 田中一之: "基礎課程・線形代数学" 培風館, 136 (1998)

    • Related Report
      1997 Annual Research Report

URL: 

Published: 1997-04-01   Modified: 2016-11-11  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi