A self-guided theorem proving system
Shie-Jue Lee · 2003
There are so many possible strategies for theorem provers to use that it becomes a problem to know how to combine them in the best way. Choosing appropriate strategies for solving a given problem may require the knowledge of different strategies or may involve a lot of painstaking trial-and-errors. To encourage the widespread use of computer reasoning systems, it is important that a reasoning system be usable by those with no knowledge of problem solving strategies, since few users have such knowledge. One possible approach is to get a lot of intelligence into a theorem proving system by having a collection of strategies and let the system by itself alternate between them. Such a system solves problems for the user automatically, freeing the user from the necessity of understanding the system or the merits of different strategies.>