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 Interfacesfor Theorm Provers. University of York, York, UK, pp. 67-74.
Available under License Creative Commons Attribution Non-commercial.
Download (71kB) | Preview
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|
|Depositing User:||Computing Research|
|Date Deposited:||07 Jul 2010 15:23|
|Last Modified:||12 Jan 2011 04:52|
Actions (login required)