I know of two algorithms for determining classical propositional validity:
Convert the problem into a SAT problem, run a SAT solver. These algorithms are efficient, but it seems difficult/infeasible to construct a formal proof of the tautology using this approach.
Brute force all truth table values. Constructing a formal proof may be feasible in some systems, but this will always take exponential time.
Is there an alternative approach for determining and proving classical propositional tautologies from basic boolean algebra laws? Dyckhoff 92 describes such an approach for intuitionistic sequent calculus (and natural deduction). Is there an equivalent result for classical propositional calculus? If not, what makes the classical case "harder"?
The method of semantic tableaux, or truth trees (which sounds friendlier), provides a proof system for classical propositional logic which easily suggests an algorithm for checking whether a formula of propositional logic is valid.
Let's do an example straight away.
Suppose you have a propositional formula, such as $p \rightarrow (q \rightarrow (p \wedge q))$ and you want to know whether it is valid in classical propositional logic. Begin by writing down the negation of the formula:
$$ \begin{align} 1 \space & \neg(p \rightarrow (q \rightarrow (p \wedge q))) \end{align} $$
There is a rule $(\alpha)$ which covers the case of a formula with the form $\neg(A \rightarrow B)$. It tells us to write down $A$ and $\neg B$ - both on the same branch as the original formula. Node $1$ is now spent or used.
$$ \begin{align} 1 \space & \neg(p \rightarrow (q \rightarrow (p \wedge q))) \\ 2 \space & p & \alpha, 1 \\ 3 \space & \neg(q \rightarrow (p \wedge q)) & \alpha, 1 \\ \end{align} $$
Node $2$ is atomic, so we can't do anything with that. Node $3$ is also susceptible to $(\alpha)$:
$$ \begin{align} 1 \space & \neg(p \rightarrow (q \rightarrow (p \wedge q))) \\ 2 \space & p & \alpha, 1 \\ 3 \space & \neg(q \rightarrow (p \wedge q)) & \alpha, 1 \\ 4 \space & q & \alpha, 3 \\ 5 \space & \neg(p \wedge q) & \alpha, 3 \\ \end{align} $$
A different rule, $(\beta)$, applies to $5$ because it is the negation of a conjunction. You will no doubt recall that, if a conjunction is false, at least one of its conjuncts is false. However, considering only this piece of information, we don't know which conjunct is false. In a truth tree, this causes the tree to branch:
$$ \begin{align} 1 \space & \neg(p \rightarrow (q \rightarrow (p \wedge q))) \\ 2 \space & p & & \alpha, 1 \\ 3 \space & \neg(q \rightarrow (p \wedge q)) & & \alpha, 1 \\ 4 \space & q & & \alpha, 3 \\ 5 \space & \neg(p \wedge q) & & \alpha, 3 \\ 6 \space \neg p \space & & 7 \space \neg q \space & \beta, 5 \\ \end{align} $$
Now there are two branches. The left branch contains $\neg p$, but also includes the earlier node $2$, which is $p$. Similarly, the right branch bears the contradictory fruit $q$ and $\neg q$. Here we apply another rule, which states that if a branch contains a propositional atom and its negation, the branch must be closed, i.e. we have nothing further to do with it. Since both branches are closed, we are done drawing the truth tree. (In a different situation, we might also have finished if there were no more 'unspent' formulae which we could apply rules to.)
Considering truth trees as proof systems, we can stipulate that a propositional formula $A$ is provable if, in drawing the truth tree for $\neg A$, every branch closes. It turns out that if $A$ is provable in this sense, then $A$ is valid. This is the soundness property of truth trees as a proof system, and it certifies that drawing truth trees algorithmically decides whether a propositional formula is valid.
I learnt about truth trees from the book Logic with Trees by Colin Howson; but I think Raymond Smullyan is to be credited for the way that book presents semantic tableaux.