STUDIES ON REASONING PRINCIPLE BASED ON LOGICAL FRAMEWORK THEORY AND ITS APPLICATION TO HEURISTIC REASONING SYSTEM

1995年，我主要研究了基于逻辑框架理论的推理原理和智能推理系统的智能语言构造。1996年，我从实现启发式推理系统的角度出发，主要研究了以下几个主题：(1)基于逻辑框架理论的人工智能语言研究：利用逻辑框架理论，研究了知识和数据的表示方法，以及有效构建系统所必需的继承机制的理论性质等问题。(2)基于类型理论的证明自动生成：研究了类型推理系统与LK序列演算之间的关系，讨论了高阶证明方法和合一理论问题。(3)基于类比的证明发现系统：在SUN工作站上使用通用定理证明语言Isabelle实现了一个推理和发现类似于人类的一阶序列演算证明的系统。通过本研究，认识到基于逻辑框架理论的方法对于形式化推理原理和智能语言是有用的。我计划将这一方法进一步扩展到人工智能。

In 1995, I have researched by focussing on the studies on the reasoning prrinciple based on the logical framework theory and intelligent language construction for intelligent reasoning systems. In 1996, I have researched mainly on the following themes from the viewpoints of inplemention of the heuristic reasoning system using the results obtained until now.(1) Studies on language for Artificial intelligence based on the logical framework theory : Using the logical framework theory, I have investigated problems such that knowledge and data representation method, and the theoretical properties of inheritance mechanism which is essential for efficient system construction. An experimental language has been implemented according to the obtained results on the SUN workstation.(2) Automatic proof generation based on the type theory : The relations between the type inference system and the LK sequent calculus has been investigated, and the problems of higher order proof method and unification theory are also discussed. Further, a method of producing a proof automaticaliy using the formulas as types principle in the type theory has been proposed and is formulated in the grammatical form.(3) Proof discovery system based on analogy : A system which reasons and discover a proof of the first order sequent calculus in the similar mannar to human beings is implemented using a general theorem proving language ISABELLE on the SUN work station.It has been recognized that the approach based on the logical framework theory is useful to formalize the reasoning principle and intelligent language through this research. I am planning to extend this approch for AI further.