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

Lowe, Helene, Cumming, Andrew, Smyth, Michael and Varey, Alison (1996) Lessons from experience: making theorem provers more co-operative. In: Proceedings of the Second Workshop on User Interfaces for Theorm Provers. University of York, York, UK, pp. 67-74.

Available under License Creative Commons Attribution Non-commercial.

Download (72kB)


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.

Item Type: Book Section
Uncontrolled Keywords: co-operative theorem proving system; user; automaton; semi-automated theorem proving system; evaluation;
University Divisions/Research Centres: Faculty of Engineering, Computing and Creative Industries > School of Computing
Dewey Decimal Subjects: 000 Computer science, information & general works > 000 Computer science, knowledge & systems > 004 Data processing & computer science
Library of Congress Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Item ID: 3265
Depositing User: Computing Research
Date Deposited: 07 Jul 2010 14:23
Last Modified: 02 Jun 2014 15:32

Actions (login required)

View Item View Item


Downloads per month over past year

View more statistics

Edinburgh Napier University is a registered Scottish charity. Registration number SC018373