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

1995 Fiscal Year Final Research Report Summary

Co-operative research on theoretical foundations of computer programs

Research Project

Project/Area Number 05302011
Research Category

Grant-in-Aid for Co-operative Research (A)

Allocation TypeSingle-year Grants
Research Field General mathematics (including Probability theory/Statistical mathematics)
Research InstitutionChiba University (1995)
University of Tsukuba (1993-1994)

Principal Investigator

TSUJI Takashi  Chiba Univ., Science Prof., 理学部, 教授 (70016666)

Co-Investigator(Kenkyū-buntansha) HITOTUMATU Shin  Tokyo Elec.Univ., Eng. Prof., 理工学部, 教授 (10027378)
ONO Hiroakira  JAIST Hokuriku, Inf.Sci. Prof., 情報科学研究科, 教授 (90055319)
NANBA Kanji  Univ.of Tokyo, Math.Sci. Prof., 大学院数理科学研究科, 教授 (40015524)
YONEDA Nobuo  Tokyo Elec.Univ., Eng. Prof., 理工学部, 教授 (50080487)
IGARASHI Shigeru  Univ.of Tsukuba, Inf.Sci. Prof., 電子情報工学系, 教授 (80027367)
Project Period (FY) 1993 – 1995
KeywordsNU / logic / theory of programs / programming / graph theory / artificial inteligence / music information processing
Research Abstract

Owing to each of research fellows, good research results are established on subjects of this research project. Some of them are listed in the following.
1.Logic : a formal derivation of the decidability of the theory SA,extending intuitionistic linear logic, the finite model property for BCK and BCIW,algebraic semantics for predicate logic, decidability and finite model property of substructural logics, a new formalization of Feferman's system, natural proofs in automated proving, validity verification of knowledge predicats.
2.Theory of programs : locomorphism analytical equivalence theory, analysis of a real time problem in a software/hardware system in two ways using nu-conversion and by tense arithmetic, literal dependence net in concurrent logic programming environment, a typed lambda-calculus of proving-by-example, a transformation method for dynamic-sized tabulation, programming by example.
3.Programming : biding time analysis for data type specialization, programming techniques for effective use of pipe-line and cache, efficiency of computing determinants by a fraction-free processor.
4.Graph theory : graph decomposition with prescribed vertices, twist number of complete bipartite praphs.
5.Artificial inteligence : a mathematical theory of machine discovery from facs, formalization of planar graphs, analysis methods and tools of expression in music performances.

  • Research Products

    (41 results)

All Other

All Publications (41 results)

  • [Publications] Shigeru Igarashi, Tetsuya Mizutani, Takashi Tsuji and Chiharu Hosono: "On locomorphism in analytical equivalence theory" Lecture Notes in Computer Science. 792. 173-187 (1994)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Kohji Tomita, Takashi Tsuji and Shigeru Igarashi: "Analysis of a Software/Hardware System by Tense Arythmetic" Lecture Notes in Computer Science. 792. 188-205 (1994)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Chiharu Hosono and Yasuo Ikeda: "A formal derivation of the decidability of the theory SA" Theoretical Computer Science. 127. 1-23 (1994)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 池田靖雄,細野千春,辻尚史: "プログラム言語BQLとその処理系" 情報処理学会論文誌. 37(印刷中). (1996)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 富田康治,辻尚史,五十嵐滋: "プログラムにおける実時間問題のν-転換による解析と動作条件" 情報処理学会論文誌. 34. 1099-1106 (1993)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Yasuhito Mukouchi and Setsuo Arikawa: "Towards a mathematical theory of machine discovery from facts" Theoretical Computer Science. 137. 53-84 (1995)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Jianjun Zhao, Jingde Cheng and Kazuo Ushijima: "Literal dependence net and its use in concurrent logic programming environment" Proceedings of the Workshop on Parallel Logic Programming attached to FGC'94. 127-141 (1994)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Jianjun Zhao, Jingde Cheng and Kazuo Ushijima: "Theoretical and experimental study of dependence-based complexity metrics for distributed programs" Proceedings of the Fourth International Conference for Young Computer Scientists. 345-352 (1995)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] R. Hori, H. Ono and H. Sshellinx: "Extending intuitionistic linear logic with knotted structural rules" Notre Dame Journal of Formal Logic. 35. 219-242 (1994)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Robert K. Meyer and Hiroakira Ono: "The finite model property for BCK and BCIW" Studia Logica. 53. 107-118 (1994)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Hiroakira Ono: "Algebraic semantics for predicate logics and their completeness" Logic at work. (to appear).

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Hiroakira Ono: "Decidability and finite model property of substructural logics" Proceedings of the Tbilisi Symposium of Language, Logic and Computation. (to appear).

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Masami Hagiya: "A Typed λ-Calculus for Proving-by-Example and Bottom-Up Generalization Procedure" Theoretical Computer Science. 137. 3-23 (1995)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Wei-Ngan Chin and Masami Hagiya: "A Transformation Method for Dynamic-Sized Tabulation" Acta Informatica. 32. 93-115 (1995)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Masami Hagiya and Tomoki Shiratori: "Programming by Example in Computing-as-Editing Paradigm" Proceedings of the 11th International IEEE Symposium on Visual Languages. 275-283 (1995)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Masami Hagiya and Kouhei Iino: "Binding Time Analysis for Data Type Specialization" Fuji International Workshop on Functional and Logic Programming. 254-269 (1995)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Mituharu Yamamoto, Shin-ya Nishizaki, Masami Hagiya and Yozo Toda: "Formalization of Planar Graphs" Lecture Notes in Computer Science. 971. 369-384 (1995)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Susumu Hayashi and Satoshi Kobayashi: "A new formalization of Feferman's system of functions and classed and its relation to Frege structure" International Journal of Foundations of Computer Science. 6. 187-202 (1995)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 大芝 猛: "自動証明における自然な証明生成への一つの近接" 情報処理学会論文誌. 35. 222-281 (1995)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 大芝猛,小橋一秀: "知識命題の標準系を用いる妥当性検証" 数理解析研究所講究録. 906. 132-135 (1995)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 前野年紀,太田昌孝: "パイプラインとキャッシュを活用するためのプログラミング技法" 第35回プログラミングシンポジウム報告集. 31-42 (1994)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Kenji Yoshida, Kunihiko Hayashi and Kazunori Miyoshi: "Programming music system “Z-MUSIC" as an texteded instrument" Proceedings of MCHA95. 1-4 (1995)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 木下孝,牧野潔夫,三好和徳: "Fraction-freeによる行列式の計算効率" 数理科学講究録. 920. 62-73 (1995)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] 一松 信: "基礎微分積分学入門" 近代科学社, (1995)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Shigeru Igarashi, Tetsuya Mizutani, Takashi Tsuji and Chiharu Hosono: "On locomorphism in analytical equivalence theory" Lecture Notea in Computer Science. 792. 173-187 (1994)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Kohji Tomita, Takashi Tsuji and Shigeru Igarashi: "Analysis of a Software/Hardware System by Tense Arythmetic" Lecture Notes in Computer Science. 792. 188-205 (1994)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Chiharu Hosono and Yasuo Ikeda: "A formal derivation of the decidability of the theory SA" Theoretical Computer Science. 127. 1-23 (1994)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Yasuhito Mukouchi and Setsuo Arikawa: "Towards a mathematical theory of machine discovery from facts" Theoretical Computer Science. 137. 53-84 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Jianjun Zhao, Jingde Cheng and Kazuo Ushijima: "Literal dependence net and its use in concurrent logic programming environment" Proceedings of the Workshop on Parallel Logic Programming attached to FGCS '94. 127-141 (1994)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Jianjun Zhao, Jingde Cheng and Kazuo Ushijima: "Theoretical and experimental study of dependence-based complexity metrics for distributed programs" Proceedings of the Fourth International conference for Young Computer Scientists. 345-352 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] R.Hori, H.Ono and H.Schellinx: "Extending intuitionistic linear logic with knotted structural rules" Notre Dame Journal of Formal Logic. 35-2. 219-242 (1994)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Robert K,Meyer and Hiroakira Ono: "The finite model property for BCK and BCIW" Studia Logica. 53. 107-118 (1994)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Hiroakira Ono: "Algebraic semantics for predicate logica and their completeness" Logic at work, E.Orlowska (ed.), Kluwer. to appear.

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Hiroakira Ono: "Decidability and finite model property of substructural logics" Proceedings of the Tbilisi Symposium of Language, Logic and Computation, CSLI,Stanford. to appear.

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Wei-Ngan Chin and Masami Hagiya: "A Transformation Method for Dynamic-Sized Tabulation" Acta Informatica. 32. 93-115 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Masami Hagiya and Kouhei Iino: "Binding Time Analysis for Data Type Specialization" Fuji International Workshop on Functional and Logic Programming, World Scientific. 254-269 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Mituharu Yamamoto, Shin-ya Nishizaki, Masami Hagiya and Yozo Toda: "Formalization of Planar Graphs" Higher-Order Logic Theorem Proving and Its Applications, Lecture Notes in Computer Science. 971. 369-384 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Susumu Hayashi and Satoshi Kobayashi: "A new formalization of Feferman's system of functions and classes and its relation to Frege structure" International Journal of Foundations of Computer Science. 6-3. 187-202 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Kenji Yoshida, Kunihiko Hayashi and Kazunori Miyoshi: "Programming music system "Z-MUSIC" as an texteded instrument" Proceedings of MCHA 95. 1-4 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Masami Hagiya and Tomoki Shiratori: "Programming by Example in Computing-as-Editing Paradigm" Proceedings of the 11th International IEEE Symposium on Visual Languages. 275-283 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Masami Hagiya: "A Typed lambda-Calculus for Proving-by-Example and Bottom-Up Generalization Procedure" Theoretical Computer Science. 137. 3-23 (1995)

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

URL: 

Published: 1997-03-04  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi