Lessons from experience: making theorem provers more co-operative.
Helene Lowe, Andrew Cumming, Michael Smyth, Alison Varey · Research Output (Edinburgh Napier University) · 1996
We describe our experiences in trying to build a co-operative theorem proving system. Our model of co-operation is that of a user and an automaton combining forces to prove theorems in a semi-automated theorem proving system. We describe various undesirable behaviours of interactive and automated systems and set out our initial objectives. We evaluate our early attempts and, in the light of this experience, draw up a tentative wish-list for future systems.