Concept formation via proof planning failure
Chapter in Scopus
- Additional Document Info
- View All
© 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  is moderately small. Using an abduction mechanism built upon proof planning , we have successfully patched 40 faulty conjectures about the HOL theory of lists . 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.