Tableau method is an algorithm in symbolic logic, to determine whether a given formula is logically true or not. In this method, we write down a diagram called analytic tableau which consists of formulas arranged by certain rules starting from the negation of the given formula. In this book, unlike the usual interpretation of analytic tableaux connected to proofs by contradiction, we give a new interpretation of analytic tableaux connected to direct proofs. By this new interpretation, we can get direct proofs for any tautologies automatically. Moreover, we get an algorithm to transform any proofs by contradiction to direct proofs.