STUDY ON INFERENCE SYSTEMS OF CONSTRUCTIVE LOGICS

构造逻辑推理系统的研究

• 批准号: 05680276
• 负责人: HIROKAWA Sachio
• 金额: $ 1.09万
• 依托单位: KYUSHU UNIVERSITY
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for General Scientific Research (C)
• 财政年份: 1993
• 资助国家: 日本
• 起止时间: 1993 至 1994
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-05680276/
• 关键词: Constructive logic; Lambda calculus; Type theory; Intuitionistic logic; Relevant logic; Curry-Howard; Formulas-as-types; Classical logic; 線形論理

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.

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

项目成果

Sachio Hirokawa,Yuichi Komori Izumi Takeuti: "A reduction rule for Peirres formule makes all the torms with the same tyyce egucl" RIFIS-TR. 91. 1-4 (1994)

Sachio Hirokawa、Yuichi Komori Izumi Takeuti：“Peirres 公式的归约规则使所有 torm 具有相同的 tyyce egucl”RIFIS-TR。

S.Hirokawa: "The number of proofs for an implicational formulas" Journal of Symbolic Logic. 58. 1117- (1993)

S.Hirokawa：“蕴涵公式的证明数量”符号逻辑杂志。

S.Hirokawa: "The relevance graph of a BCK-formula" Journal of Logic and Computation. 3. 269-285 (1993)

S.Hirokawa：“BCK 公式的相关图”逻辑与计算杂志。

Sachio Hirokawa: "Infiniteness of proof(α→α) is polynomial-spaie complete" RIFIS-TR. 92. 1-11 (1994)

Sachio Hirokawa：“无限证明（α→α）是多项式空间完备的”RIFIS-TR。 92. 1-11 (1994)

Y.Komori: "Syntactic Investigations into BI Logic and BB'I Logic" Studia Logica. Vol.53. 397-416 (1994)

Y.Komori：“BI 逻辑和 BBI 逻辑的句法研究”Studia Logica。