|
|||||
|
|
TPS: A hybrid automatic-interactive system for developing proofs |
|
| Authors: | Peter B. Andrews Chad E. Brown |
| Affiliation: | aDepartment of Mathematical Sciences, Carnegie Mellon University, Pittsburgh, PA, USA;bUniversität des Saarlandes, Saarbrücken, Germany |
| 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. |
| Keywords: | smCaps" >Tps Theorem proving system Automatic proofs Semi-automatic proofs Semi-interactive proofs Interactive proofs Type theory Higher-order logic First-order logic Automating mathematics Mathematics assistance system |
| 本文献已被 ScienceDirect 等数据库收录！ | |