\code{
\func{PL-Resolution}{\v{KB}{\ac}\(\alpha\)}{\v{true} or \v{false}}
    \firstinputs{\v{KB}}{the knowledge base, a sentence in propositional logic}
    \inputs{\(\alpha\)}{the query, a sentence in propositional logic}
\bodysep
    \setq{\v{clauses}}{the set of clauses in the CNF representation of \(\v{KB}\land\lnot\alpha\)}
    \setq{\v{new}}{\(\{\,\}\)}
    \k{loop do}
          \k{for each} \(C_i\), \(C_j\) \k{in} \v{clauses} \k{do}
                \setq{\v{resolvents}}{\prog{PL-Resolve}(\(C_i\){\ac}\(C_j\))}
                \k{if} \v{resolvents} contains the empty clause \k{then return} \v{true}
                \setq{\v{new}}{\(\v{new}\union \v{resolvents}\)}
          \k{if} \(\v{new}\subseteq\v{clauses}\) \k{then return} \v{false}
          \setq{\v{clauses}}{\(\v{clauses}\union\v{new}\)}
%% \fnsep
%% \func{PL-Resolve}{{\mathdelim}C_1{\mathdelim}{\ac}{\mathdelim}C_2{\mathdelim}}{a set of clauses}
%%     \firstinputs{{\mathdelim}C_1{\mathdelim}{\ac}{\mathdelim}C_2{\mathdelim}}{two clauses, each viewed as a set of literals}
%%     \setq{\v{resolvents}}{{\mathdelim}\{\,\}{\mathdelim}}
%%     \k{for each} {\mathdelim}l_i{\mathdelim} \k{in} {\mathdelim}C_1{\mathdelim} and {\mathdelim}m_j{\mathdelim} \k{in} {\mathdelim}C_2{\mathdelim} \k{do}
%%           \k{if} {\mathdelim}l_i{\mathdelim} and {\mathdelim}m_j{\mathdelim} are complementary literals \k{then do}
%%                 \setq{\v{C}}{{\mathdelim}(C_1 - l_i)\union (C_2 - m_j){\mathdelim}}
%%                 \setq{\v{resolvents}}{{\mathdelim}\v{resolvents}\union \{C\}{\mathdelim}}
%%    \k{return} \v{resolvents}
}

