Co-operative Theorem Proving

Helen Lowe, Napier University, Edinburgh, Scotland

Abstract:

For the forseeable future, there will be theorems which cannot be proved completely automatically, so the ability to allow human intervention is desirable; for this intervention to be productive the problem of orienting the user in the proof attempt must be overcome. There are many semi-automatic theorem provers: we call our style of theorem proving co-operative, in that the skills of both human and automaton are used each to their best advantage, and used together may find a proof where other techniques fail. We are developing BARNACLE, a co-operative interface to the CLAM inductive theorem proving system. The co-operative nature of the BARNACLE interface is made possible by the proof planning technique underpinning CLAM. We are extending BARNACLE to other domains. We have a prototype equation solving system and are considering integration as a promising test bed for these techniques.