STUDY ON INFERENCE SYSTEMS OF CONSTRUCTIVE LOGICS

给出了公式与计算规则之间的对应关系的形式化系统。这种对应扩展了公式作为类型的概念，而公式作为类型的概念是函数式程序设计语言和从构造性证明中抽取程序的基础。这个公式是经典逻辑的特征。我们得到的约简规则不仅从逻辑角度看有自然的意义，而且从经典证明的程序抽取角度看也有自然的意义。得到了约化的几个性质。也发现了与延拓计算的相似性。进一步的分析是必要的。以下是直觉逻辑之下的子结构逻辑的结果的选择。小森利用根岑系统对关联逻辑中的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.