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.

  • Date:

    01 January 1996

  • Publication Status:

    Published

  • Library of Congress:

    QA75 Electronic computers. Computer science

  • Dewey Decimal Classification:

    004 Data processing & computer science

Citation

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

Authors

Keywords

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

Monthly Views:

Available Documents