TPS, the "Theorem Proving System" was the first automated theorem prover for higher-order logic (called "simple type theory" by Peter Andrews, the principal of the TPS project).
The TPS library contains almost all theorems from Peter Andrew's Book An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof and a variety of other examples that have been proven in the project. It has been converted to OMDoc by Chad E. Brown in 2002.
Sadly, the TPS library in MathHub.info does no contain any proofs, even though TPS could in principe generate them. Volunteers please contact Michael Kohlhase.
Responsible: firstname.lastname@example.org, email@example.com
- Size: K
- The TPS Library the main library of the TPS theorem prover, it has been converted to OMDoc by Chad E. Brown in 2002.