| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 4663132 | Journal of Applied Logic | 2006 | 29 Pages |
Abstract
The theorem proving system Tps provides support for constructing proofs using a mix of automation and user interaction, and for manipulating and inspecting proofs. Its library facilities allow the user to store and organize work. Mathematical theorems can be expressed very naturally in Tps using higher-order logic. A number of proof representations are available in Tps, so proofs can be inspected from various perspectives.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
Peter B. Andrews, Chad E. Brown,