权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

STRUCTURE OF INFERENCE IN CONSTRUCTIVE LOGICS

构造逻辑中的推理结构

基本信息

批准号：
07680364
负责人：
HIROKAWA Sachio
金额：
$ 1.34万
依托单位：
KYUSHU UNIVERSITY
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
1995
资助国家：
日本
起止时间：
1995 至 1997
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-07680364/
关键词：
LANBDA-CALCULUS TYPE THEORY RELEVANT LOGIC CLASSICAL LOGIC 構成的論理証明システム線型論理

项目摘要

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.

构造逻辑是一种通过证明规范的正确性来实现程序构造的逻辑。lambda项是函数式程序的常用实现。在计算机系统中，证明被表示为一系列推理规则。我们用项作为这些证明的一种形式。我们分析了推理和证明图形的结构以及证明的转换。我们得到了以下结果。相关逻辑：我们形式化了相关逻辑P-W的证明。证明被描述为遗传的右极大线性λ项。我们证明了定理*在P-W中只有平凡的证明。经典逻辑的λ演算：我们扩展了λ演算，并将经典逻辑公式化为该演算的类型系统。我们发现了微积分中的一个计算规则，并证明了同一个公式的任意两个证明都可以在微积分中被识别。通过对Peirce公式的仔细分析，得出了计算规律。我们用Parigot证明了微积分和微积分之间的关系。证据检索系统；我们证明了直觉逻辑中的证明集可以用类似上下文无关的语法来描述。我们展示了从给定公式构造语法的算法。通过对这种语法结构的分析，我们证明了证明的无穷性是多项式空间完备的。我们实现了证明搜索算法。该系统以java applet的形式提供。