Solving SAT using tableau calculus
It can be, but the solution process is equivalent to converting a CNF formula to DNF, which is NP-hard.  You will at worst end up exploring an exponential number of disjunction branches.