System dowodzenia twierdzeń
Theorem Proving System (TPS) to zautomatyzowany system dowodzenia twierdzeń dla logiki pierwszego i wyższego rzędu . TPS został opracowany na Uniwersytecie Carnegie Mellon . Jego edukacyjna wersja jest znana jako ETPS ( Educational Theorem Proving System ).