Extending the proof methods and critics of a proof planner
Daniel Raggi · 2011
We analysed the failed proof attempts of the proof planner IsaPlanner, searching for patterns that would help us design methods and critics or extend those already implemented in IsaPlanner. The analysis led to a classification, of which two classes had already been discovered and discussed before. A broad novel class was found, in which multiple applications of the inductive hypothesis were required to complete the proofs. The fitted extension to IsaPlanner’s methods was designed and implemented successfully. Our results are presented and discussed.