We provide techniques to integrate resolution logic
in type theory. The results may be rendered as follows.

- A clausification procedure in type theory, equipped
with a correctness proof, all encoded using higher-order primitive recursion.

- A translation of resolution proofs into lambda terms,
yielding a verification procedure for those proofs.

- The power of resolution theorem provers becomes available in
interactive proof construction systems based on type theory.