STRUCTURE OF INFERENCE IN CONSTRUCTIVE LOGICS
Project/Area Number  07680364 
Research Category 
GrantinAid for Scientific Research (C)

Section  一般 
Research Field 
計算機科学

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

CoInvestigator(Kenkyūbuntansha) 
KOMORI Yuichi CHIBA UNIVERSITY,DEPATMENT OF MATHEMATICS,PROFESSOR, 理学部, 教授 (10022302)

Project Fiscal Year 
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)

Keywords  LANBDACALCULUS / TYPE THEORY / RELEVANT LOGIC / CLASSICAL LOGIC / ラムダ計算 / 型理論 / 適切さの論理 / 古典論理 / 構成的論理 / 証明システム / 線型論理 
Research Abstract 
Constructive Logic is a logic which enables program construction from the proof of correcteness of specification. Lambdaterms are commonly used implementation of functional programs. In computer systems, the proofs are represented as a series of inference rules. We use the lambdaterms 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 PW.The proofs are characterized as Hereditary RightMaximal Linear lambodaterms. We showed that the theorem alpha*alpha has only trivial proof in PW. Lambdacalculus for Classical Logic : We extended the lambdacalculus 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 lambdamucalculus by Parigot. Proof Search System ; We proved that the set of proofs in intuitionistic logic can be described by a contextfree 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 polynomialspace complete. We inplemented the proof search algorithm. The system is available as Jave applet.

Report
(5results)
Research Output
(18results)