Is it possible to discover new kinds of proof in a proof planning system?
Since general-purpose proof plans represent common patterns in proofs then, by definition, they cannot discover new kinds of proof. This limitation could be overcome in several ways. One would be to include a default method which invoked some general search technique. This might find a new kind of proof by accident. Another might be to have meta-methods which constructed new methods. For instance, a method for one domain might be applied to another by generalising its preconditions. [Often new departures come in mathematics when mathematicians switch from one area to another bringing their proof methods with them.] Or a method might be learnt from an example proof (see the answer about learning new proof plans for more information). Proof plans might, for instance, be learnt from proofs constructed by general search. • Isn’t totally automated theorem proving infeasible? For the foreseeable future theorem provers will require human interaction to guide the search for non-trivial proofs.
Related Questions
- Is it possible to procure the Clampcrete system components separately from different sources and still achieve the certified crash-tested system?
- Is it possible to purchase the hardcopy courseware for the 50217 Planning and Deploying Microsoft® System Center Service Manager 2010?
- Is it possible to integrate ProSched with ERP or Plant Information System?
