STUDY ON INFERENCE SYSTEMS OF CONSTRUCTIVE LOGICS

得到了公式与计算规则对应的形式化系统。这种对应关系扩展了“公式即类型”的概念，该概念是函数式编程语言和从构造证明中提取程序的基础。在直觉逻辑之上的一个重要发现是皮尔斯公式的约化规则。这个公式是经典逻辑的特征。所得到的约简规则不仅从逻辑的角度看具有自然意义，而且从经典证明的程序提取上看也具有自然意义。得到了还原的几个性质。并发现了与延拓计算的相似性。进一步分析是必要的。以下是直觉逻辑下的子结构逻辑的结果选择。小森运用根岑系统对相关逻辑中的P-W问题给出了清晰的句法证明。Hirokawa描述了与P-W中证明相对应的λ项，并澄清了P-W中证明的结构。在与M.Takahashi和Y.Akama的联合工作中，Hirokawa获得了直觉主义逻辑中一个公式的证明集的描述，作为一个类似上下文自由的语法。

A formal system was obtained for the correspondence between formulas and computation rules. This correspondence extends the Formulas-as-type notion which is a basis of functional programming languages and program extraction from the constructive proofs.An essential discovery above the intuitionistic logic was the reduction rule for Peirce formula. This formula characterises the classical logic. The reduction rule we obtained has natural meaning not only from logical view point but also from program extraction using classical proofs. Several properties of the reduction were obtained. The similarity to the continuation computation was found as well. Further analysis is necessary.The following are the selection of the result for substructural logics below intuitionistic logic. Komori gave a clear syntactic proof for the P-W problem in relevant logic by applying Gentzen system. Hirokawa characterised the lambda-terms that correspond to the proofs in P-W and clarified the structure of the proofs in P-W.In the joint work with M.Takahashi and Y.Akama, Hirokawa obtained a description of the set of proofs for a formula in intuitionistic logic as a context-free-like grammar.