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'.