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

Lowe, Helene; Cumming, Andrew; Smyth, Michael; Varey, Alison

Abstract

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.

Citation

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

• Conference Name: 2nd Workshop on User Interfaces for Theorm Provers
• Publication Date: 1996
• Deposit Date: Jul 7, 2010
• Publicly Available Date: Jul 7, 2010
• Peer Reviewed: Peer Reviewed
• Pages: 67-74
• Book Title: Proceedings of the Second Workshop on User Interfaces for Theorm Provers
• Keywords: co-operative theorem proving system; user; automaton; semi-automated theorem proving system; evaluation
• Public URL: http://researchrepository.napier.ac.uk/id/eprint/3265