STRUCTURE OF INFERENCE IN CONSTRUCTIVE LOGICS

点击翻译按钮获取中文摘要

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.