TPS
TPS, standing for Theorem Proving System, is a theorem prover for first-order logic and type theory. A restricted version, ETPS, is intended for students and contains only commands relevant to proving theorems interactively.

TPS is available under a license that does not qualify as 'free'.

Theorem Provers Application Mathematics