1997 Fiscal Year Final Research Report Summary
STRUCTURE OF INFERENCE IN CONSTRUCTIVE LOGICS
| Project/Area Number |
07680364
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | KYUSHU 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
|
| Keywords | LANBDA-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.
|
