Research On Tableau Basic Theory And Application

One of the extension of Automated Theory Proving(ATP)—Automated Reasoning (AR) is basis work of AI.Reasoning system is regarded as the key part in many important AI system.So research of AR will exert a tremendous influence to the other branches of AI. The reasoning methods that rise by AR have been applied widespreadly.Semantic tableau was put forward by Beth(1959),Hintikka(1955),and then be introduction to automated theorem proving.For the different logic system,the tableau rules are the same,only to expand the formula structure set to make it closer to the logic of the system.As the tableau method is highly versatile and intuitive,from the beginning of the 1960s,caused computer scientists(represented by Smullyan,Fitting) interested in,as the same as resolution, it is considered to be important AR methods.Especially in the past 10 years,attracted more attention,many people in the search for a variety of the ways of tableau.In this paper,on the basis of research the basic theory of proposition and first-order logic,focus on the following five point:1.On the basis of research the basic expression of the logic,focus on the notation of the normal formulas and use Prolog language to archieve;2.On the basis of semantic of logic,focus on the reasoning of tableau,and improve it, then prove the validity and completeness;3.On the basis of expand the basic tableau,focus on the tableau with equality;4.Apply the basic theory and method of tableau to repair the database,which can solve some problems that in the traditional methods;5.Use Prolog language to archieve the theories and methods which mentioned above.