\begin{definition}[Definition:Decision Procedure]
Let $S$ be a set of propositional formulas.
A '''decision procedure for $S$''' is an algorithm which, given a propositional formula $\mathbf A$, always terminates, returning the answer:
* '''Yes''' if $\mathbf A \in S$;
* '''No''' if $\mathbf A \notin S$.
\end{definition}