| TPS: A Theorem Proving Systemfor Classical Type Theory (2008) | |||||||||||||||
Abstract | |||||||||||||||
| AbstractThis is a description of T PS, a theorem proving system for classical type theory (Church's typedl-calculus). T PS has been designed to be a general research tool for manipulating wffs of first- andhigher-order logic, and searching for proofs of such wffs interactively or automatically, or in a combination of these modes. An important feature of TPS is the ability to translate betweenexpansion proofs and natural deduction proofs. Examples of theorems that T | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||