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

STRUCTURE OF INFERENCE IN CONSTRUCTIVE LOGICS

Research Project

Project/Area Number 07680364
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field 計算機科学
Research InstitutionKYUSHU UNIVERSITY

Principal Investigator

HIROKAWA Sachio  KYUSHU UNIVERSITY,COMPUTER CENTER,PROFESSOR, 大型計算機センター, 教授 (40126785)

Co-Investigator(Kenkyū-buntansha) KOMORI Yuichi  CHIBA UNIVERSITY,DEPATMENT OF MATHEMATICS,PROFESSOR, 理学部, 教授 (10022302)
Project Period (FY) 1995 – 1997
Project Status Completed (Fiscal Year 1997)
Budget Amount *help
¥2,100,000 (Direct Cost: ¥2,100,000)
Fiscal Year 1997: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 1996: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 1995: ¥600,000 (Direct Cost: ¥600,000)
KeywordsLANBDA-CALCULUS / TYPE THEORY / RELEVANT LOGIC / CLASSICAL LOGIC / 構成的論理 / 証明システム / 線型論理
Research Abstract

Constructive Logic is a logic which enables program construction from the proof of correcteness of specification. Lambda-terms are commonly used implementation of functional programs. In computer systems, the proofs are represented as a series of inference rules. We use the lambda-terms as a form of those proofs. We analyzed the structure of inference and proof figures as well as the transformation of proofs.
We obtained the following results.
Relevant Logics :
We formalised the proof for the relevant logic P-W.The proofs are characterized as Hereditary Right-Maximal Linear lamboda-terms. We showed that the theorem alpha*alpha has only trivial proof in P-W.
Lambda-calculus for Classical Logic :
We extended the lambda-calculus and formulated classical logic as type system for the calculus. We discovered a computation rule in the calculus and showed that any two proofs of the same formula are identified in the calculus. The computation rule are obtained from the carefull analysis of Peirce formula. We showed the relation between this calculus and lambda-mu-calculus by Parigot.
Proof Search System ;
We proved that the set of proofs in intuitionistic logic can be described by a context-free like grammar. We showed the algorithm that construct the grammar from given formula. With the analysis of this grammar structure, we showed that the infiniteness of proof is polynomial-space complete. We inplemented the proof search algorithm. The system is available as Jave applet.

Report

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

    (18 results)

All Other

All Publications (18 results)

  • [Publications] Sachio Hirokawa: "Right Weakening and Right Contradion in LK" Australian Conputer science Communication. 18. 168-174 (1996)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Masako Takahashi, Youji Akama, Sachio Hirokawa: "Normal proots and their grammars" Information and computation. 125. 144-153 (1996)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Sachio Hirokawa: "The proof of α→α in P-W" Journal of Symbolic Logic. 61. 195-211 (1996)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Sachio Hirokawa, Yuichi Komori, Izumi Takeuti: "A reduction rule for peirce formula" Studia Logica. 56. 419-426 (1996)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Sachio Hirokawa: "Infiniteness of proot(α)is polynomicl-space complete" Theoretical Computer Ccience. (印刷中).

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Sachio Hirokawa: "Right Weakening and Right Contraction in LK" Australian computer Science Communications. 18(3). 168-174 (1996)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Masako Takahashi, Youji Akama, Sachio Hirokawa: "Normal proofs and their grammars" Information and Computation. 125(2). 144-153 (1996)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Sachio Hirokawa: "The proof of alpha*alpha in P--W" Journal of Symbolic Logic. 61(1). 195-211 (1996)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Sachio Hirokawa, Yuichi Komori, Izumi Takeuti: "A reduction rule for the Peirce formula" Studia Logica. 56(3). 419-426 (1996)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Sachio Hirokawa: "Infiniteness of proof (^<\alpha>) is polynomial-space complete" Theoretical Computer Science. (in press).

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Sachio Hirokawa: "Infiniteness of proof(α) is Polynomial-space complete" Theoretical Computer Science. (印刷中).

    • Related Report
      1997 Annual Research Report
  • [Publications] Sachio Hirokawa: "The proof of a→a in P-W" Journal of Symbolic Logic. 61・1. 195-221 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] Sachio Hirokawa: "A reduction rule for the Peirce formula" Studia Logica. 56・3. 419-426 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] Masako Takahashi: "Normal Proofs and Their Grammars" Information and Computation. 125・2. 144-153 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 佐塚秀人: "分散する証明推論エンジンのWEB上での結合について" マルチメディアと分散処理ワークショップ論文集. 341-348 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] I. Takeuti, S. Hirokawa: "A functional culculus of implication" Proceedings of 10th LMPS. 50-50 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] S. Hirokawa: "Right weakening and right contraction in LK" Australian Computer Science Communications. 18. 168-174 (1996)

    • Related Report
      1995 Annual Research Report
  • [Publications] Y. Komori: "Syntactic Investigations into BI and BB'I Logic" Studia Logica. 53. 397-416 (1994)

    • Related Report
      1995 Annual Research Report

URL: 

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

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi