STUDY ON INFERENCE SYSTEMS OF CONSTRUCTIVE LOGICS

得到了公式与计算规则对应的形式化系统。这种对应关系扩展了函数式编程语言和从构造性证明中提取程序的基础公式as-type概念。在直觉逻辑之上的一个重要发现是Peirce公式的约简规则。这个公式是经典逻辑的特征。我们得到的约简规则不仅从逻辑上看具有自然意义，而且从使用经典证明的程序提取中也具有自然意义。得到了该还原的几个性质。同时也发现了与延拓计算的相似性。下面是直觉主义逻辑下子结构逻辑结果的选取。小森运用Gentzen系统对相关逻辑中的P-W问题给出了清晰的句法证明。Hirokawa刻画了P-W中与证明相对应的lambda项，并阐明了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.