STRUCTURE OF INFERENCE IN CONSTRUCTIVE LOGICS

构造性逻辑是一种通过证明规格说明的正确性来构造程序的逻辑。lambda项是函数式程序的常用实现。在计算机系统中，证明被表示为一系列推理规则。我们使用了这些证明的一种形式，我们分析了推理图和证明图的结构以及证明图的变换，得到了以下结果：相关逻辑：我们对相关逻辑P-W的证明进行了形式化，证明被刻画为遗传右极大线性λ项。我们证明了定理alpha*alpha在P-W.经典逻辑的λ演算中只有平凡的证明：我们扩展了λ演算，并将经典逻辑公式化为演算的类型系统。我们发现了微积分中的一个计算规则，并证明了同一公式的任何两个证明在微积分中是相同的。通过对Peirce公式的详细分析，得出了计算规则.证明搜索系统证明了直觉逻辑中的证明集可以用上下文无关的类文法来描述。给出了由给定公式构造文法的算法。通过对这种文法结构的分析，我们证明了其无穷性证明是多项式空间完备的。我们实现了证明搜索算法。该系统可作为Java applet使用。

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.