DTP Prover
DTP (Don's Theorem Prover) is "a sound and complete inference engine for first-order predicate calculus. It specializes in domain-independent control of inference."

The source and documentation for DTP is available here: http://www.cs.cmu.edu/afs/cs.cmu.edu/project/ai-repository/ai/areas/reasonng/atp/systems/dtp/0.html

Application, Theorem Provers, CMU AI Repository