Research Output

Lessons from experience: making theorem provers more co-operative.

  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.

  • Type:

    Book Chapter

  • Date:

    30 November 1995

  • Publication Status:


  • Publisher

    University of York

  • Library of Congress:

    QA75 Electronic computers. Computer science

  • Dewey Decimal Classification:

    004 Data processing & computer science


Lowe, H., Cumming, A., Smyth, M. & Varey, A. (1995). Lessons from experience: making theorem provers more co-operative. In Proceedings of the Second Workshop on User Interfaces for Theorm Provers, 67-74. University of York



co-operative theorem proving system; user; automaton; semi-automated theorem proving system; evaluation;

Monthly Views:

Available Documents