\begin{definition}[Definition:Decision Procedure/Refutation Procedure]
Given a decision procedure for satisfiability, one can craft a decision procedure for tautologies in the following way:
Suppose one wanted to decide if a propositional formula $\mathbf A$ is a tautology.
Then apply the given procedure to decide if its negation $\neg \mathbf A$ is satisfiable.
Now:
:If $\neg \mathbf A$ is not satisfiable, then by Tautology iff Negation is Unsatisfiable, $\mathbf A$ is a tautology.
:If $\neg \mathbf A$ is satisfiable, then by Satisfiable iff Negation is Falsifiable, $\mathbf A$ is falsifiable, so cannot be a tautology.
Hence we have crafted a decision procedure for tautologies.
Such a procedure is called a '''refutation procedure''', because it proceeds by refuting, i.e. proving unsatisfiability of the negation of the formula at hand.
\end{definition}