8 Th International Workshop User Interfaces for Theorem Provers (uitp'08) Tphols'08 Satellite Workshop List of Contributions an Interactive Driver for Goal Directed Proof Strategies Managing Proof Documents for Asynchronous Processing a Lightweight Theorem Prover Interface for Eclipse Panoptes: an E

– Informal Workshop Proceedings – Preface The User Interfaces for Theorem Provers workshop series brings together researchers interested in designing, developing and evaluating interfaces for interactive proof systems, such as theorem provers, formal methods tools, and other tools manipulating and presenting mathematical formulas. While the reasoning capabilities of interactive proof systems have increased dramatically over the last years, the system interfaces have often not enjoyed the same attention as the proof engines themselves. In many cases, interfaces remain relatively basic and under-designed. The User Interfaces for Theorem Provers workshop series provides a forum for researchers interested in improving human interaction with proof systems. We have solicited contributions from the theorem proving, formal methods and tools, and HCI communities, both to report on experience with existing systems, and to discuss new directions. The topics covered by the workshop include, but are not limited to: – Application-specific interaction mechanisms or designs for prover interfaces – Experiments and evaluation of prover interfaces – Languages and tools for authoring, exchanging and presenting proof – Implementation techniques (e.g. web services, custom middleware, DSLs) – Integration of interfaces and tools to explore and construct proof – Representation and manipulation of mathematical knowledge or objects – Visualization of mathematical objects and proof – System descriptions UITP 2008 is a one-day workshop held on Friday, August 22nd 2008 in Montréal, Canada, as a TPHOLS'08 workshop. Eight papers have been selected by the international programme committee for presentation at the workshop. Additionally, we have two invited system demonstrations, one by Matt Kaufmann and J Strother Moore on interface aspects of the ACL2 theorem proving system and one by Sam Owre on the PVS user interfaces. Finally, Deborah McGuinness demonstrates an explanation infrastructure for TPTP proofs and solicits feedback. We cordially thank the following programme committee members for their valuable work and support: Finally, we thank the organizers of TPHOLs'08,Sofì ene Tahar, Otmane Ait-Mohamed and César Muñoz, for their collaboration and help with respect to the organization of UITP'08 in Montreal, Canada. In the managing of the whole reviewing process, Andrei Voronkov's EasyChair conference management system proved itself an excellent tool. Abstract Interactive Theorem Provers (ITPs) are tools meant to assist the user during the formal development of mathematics. Automatic proof searching procedures are a desirable aid, and most ITPs supply the user with an extensive set of facilities to improve automation. However, the black-box nature of most automatic procedure …