An Inquiry Into Tableau Calculus

Tab leu calculus is a logic style. It is very consistent with the intuition, and joins the proof theory and semantics of a logic system together very well. Now it is causing people more and more attention.The dissertation cobms and states briefly the history of tableau calculus firstly. The mothed of therom-proving in tableau calculus calls tableau method. The idea of the tableau method derives from Gentzen, growing through Beth, Hintikka and others, and being matured by Smullyan at last. Now this method is used in many logics.Then the dissertation gives some systems classical and non-classical logic, at the same time discuss the meta-logic property of every system, the proof of the tableau system of first order logic shows that there are important differences between the proof of tableau systems and axiomatic systems, for tableau systems, whether they have confluence property can also influence the completeness proofAt last we compare the tableau calculus with sequent calculus, natural deduction and others, reveals the advantages and disadvantages of each style. The invention of tableau systems will continue, because they are easier to think than other formulations. The increasing interest in non-classical theorem-proving has brought tableaus to a position of prominence, because they exist for many logics. The development of tableau systems will as important as the research of logic itself...