An integral theorem prover and the role of proof planning |
| |
Authors: | James D Baker Shahriar Zand-Biglari |
| |
Affiliation: | (1) Research and Development, Lockheed Missiles & Space Company, Inc., 3251 Hanover Street, 94304-1187 Palo Alto, CA, USA;(2) Department of Computer Science, University of Texas at Austin, 78712 Austin, TX, USA |
| |
Abstract: | An investigation is made into the ways proof planning can enhance the capability of a rule based prover for the theory of integration. The integrals are of the Riemann type and are defined in a way to maximize the theorem proving methods of predicate calculus. Approximately fifty theorems have been proved and several examples are discussed. A major shortcoming was found to be the inability of the system to work with or produce a proof plan. As a result, a planning scheme based on the idea of subgoals or milestones was considered. With user defined plans, there was a substantial increase in performance and capability of the system and, in some cases, proofs which were previously unsuccessful were completed. |
| |
Keywords: | Automated theorem proving integration planning |
本文献已被 SpringerLink 等数据库收录! |
|