\begin{tabbing}
XXXX\=XXXX\=XXXX\=XXXX\= \kill  % set up a few tab stops
{\bf function} {\tt HORN}\,($\phi$):\\
\hbox{/* precondition: \(\phi\) is a Horn formula */}\\
\hbox{/* postcondition: \({\tt HORN}\,(\phi)\)
decides the satisfiability for $\phi$ */}\\
{\bf begin function}\\
\> mark all occurrences of \(\top\) in \(\phi\);\\
\> {\bf while} there is a conjunct $P_1\land P_2\land \dots
                                      \land P_{k_i}\to P'$ of $\phi$\\
\>\> such that all $P_j$ are marked  but $P'$ isn't {\bf do}\\
\>\> mark $P'$\\
\> {\bf end while}\\
\> {\bf if} $\bot$ is marked {\bf then return} `unsatisfiable' {\bf else
return} `satisfiable'\\
{\bf end function}
\end{tabbing}