This set of programs in Caml-Light gives some examples of algorithms in logic: some validity tests for propositionnal formulas, first-order unification (including pseudo-linear), resolution for predicate calculus.
You can download