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

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

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.