ChapterSCO_84937406344

abstract

• © Springer-Verlag Berlin Heidelberg 2001. The analysis of failed proof attempts is central to concept formation. This process essentially makes use of abduction, a form of reasoning that identifies explanations for an observed phenomenon. The main problem with abduction is the combinatorial explosion: the search space originated from a failed proof attempt is often unmanageable. A careful proof search guidance is thus required to enable a successful analysis of failure. Fortunately, the search space generated by proof planning [6] is moderately small. Using an abduction mechanism built upon proof planning [18], we have successfully patched 40 faulty conjectures about the HOL theory of lists [3]. On each faulty conjecture, our mechanism was able to synthesise a condition that turns the conjecture into a theorem. Each condition proved to be a concept that is known to be useful and interesting. This process is a form of concept formation. Concept formation was done automatically. Once refined, the conjectures can then be used to write a fast, uniform proof procedure for proving properties of list constants without effort.