- cl-unification - Provides unification (as used in Prolog) over fairly arbitrary Common Lisp objects
- Prolog Technology Theorem Prover - The Prolog Technology Theorem Prover (PTTP) is an implementation (in Common Lisp) of the model elimination theorem-proving procedure that extends Prolog to the full first-order predicate calculus

unification

Libraries adding unification operations to Common Lisp