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 (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
    Item ID: 3265
    Depositing User: Computing Research
    Date Deposited: 07 Jul 2010 15:23
    Last Modified: 02 Jun 2014 16:32

    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...

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