Study On Optimization Of Technology Of The Proof Device Based On Tableau

The semantic Tableau is a strong intuitive and practical reasoning method. Since the method was put forward, it has attracted a majority of artificial intelligence researchers. Basing on the Prolog language and the use of semantic Tableau method, M.C.Fitting proposed a first-order logic theorem prover. As we all know, the efficiency problem of a system is a hot issue in the research area of artificial intelligence. Although the theorem prover presented by M.C.Fitting is easy to understand, it still exists some efficient problems in the concrete application. This paper is aiming at this problem to carry out specific research. The specific research contents are as follows:1 This paper gives formulas, clauses, and related concepts of the first-order logic language. Basing on those, it studys the theory, the system model of this language, and especially it pays more attention to the Herbrand model of the language.2 It introduces the theory and implementation of the semantic Tableau method. First, it gives a brief description of the Tableau concept and the semantic Tableau expansion rules in the process of its practical application, and at the same times it completes the demonstrations of the soundness and completeness of the method. Second, this paper provides the algorithm of this system and gives the code of it by using the Prolog language.3 Analysis is carried out to study the efficiency problem of the former prover, and it puts forward a relevant improvement and the improved algorithm. What the most important thing is that the termination and correctness of the algorithm are proved. Finally, by the comparison corresponding experiment, the results show that the optimized theorem prover semantic Tableau improves greatly in time efficiency of deduction.