| Strategic Issues Related to the Development and Use of TPS (2007) | |||||||||||||||||
Abstract | |||||||||||||||||
| nsion trees and matings (using ideas described in [1] and [3]), but TPS proofs are presented in natural deduction style, and TPS can operate in a mixture of interactive and automatic modes [6]. Many strategic decisions were involved in the development of TPS, and many more are made (by setting various flags) when one uses TPS to search for a proof of a theorem. Other strategic questions arise when one considers how more diverse methods of proof search might be integrated with those already implemented in TPS. Relevant work [8] on integrating TPS into the\Omega MEGA system [7] is already being done. It is also valuable to try to understand what the strategies used for other methods of proof search mean from the perspective of expansion proofs and matings. Ultimately, we wish to understand how fundamental ideas about strategies manifest themselves in a variety of theorem-proving contexts. References | |||||||||||||||||
Publication details | |||||||||||||||||
| |||||||||||||||||