컴퓨터에 의한 자동적인정리증명에 관한 연구

Abstract

In this paper first we describe the general concepts of automatic theorem proving and discuss the applications of it. Then we investigate the historical stage of developments in automatic theorem proving methods, examine and compare the various modern automatic theorem proving methods and discuss the merits and the defects of them. Then we describe a sample theorem and the conversion process of it into logical standard forms and show a proof example of the logical standard forms by an automatic theorem prover in computer. Consequently, we proposed the future research directions on the refinements of automatic theorem proving methods.

In this paper first we describe the general concepts of automatic theorem proving and discuss the applications of it. Then we investigate the historical stage of developments in automatic theorem proving methods, examine and compare the various modern automatic theorem proving methods and discuss the merits and the defects of them. Then we describe a sample theorem and the conversion process of it into logical standard forms and show a proof example of the logical standard forms by an automatic theorem prover in computer. Consequently, we proposed the future research directions on the refinements of automatic theorem proving methods.