UITP on Monday, August 21st

Session 1 (09:00‑10:30)

09:00‑09:30	Julien Narboux (LIX - INRIA FUTURS, France) A Graphical User Interface for Formal Proofs in Geometry. We present in this paper the design of a graphical user interface to deal with proofs in geometry. The software developed combines three tools: a dynamic geometry software to explore, measure and invent conjectures, an automatic theorem prover to check facts and an interactive proof system (Coq) to mechanically check proofs built interactively by the user.
09:30‑10:00	Pedro Quaresma (Department of Mathematics, School of Science and Technology, University of Coimbra) Predrag Janicic (Faculty of Mathematics, University of Belgrade) GeoThms - a Web System for Euclidean Constructive Geometry GeoThms is a web-based system that integrates Automatic Theorem Provers (ATP), Dynamic Geometry Software (DGS) and a database, providing a framework for exploring geometrical knowledge. The GeoThms user can easily use/browse through existing geometrical content and also build new content on his-her own. In this paper we describe GeoThms functionalities focusing in the interface solutions required for a system aimed at supporting studying and teaching geometry. GeoThms is an publicly accessible system, we believe that, with the help of all its users, it will became an important Internet resource for geometry.
10:00‑10:30	Claudio Sacerdoti Coen (University of Bologna) Enrico Tassi (Department of Computer Science, University of Bologna) Stefano Zacchiroli (Computer Science Department, University of Bologna) Tinycals: step by step tacticals Most of the state-of-the-art proof assistants are based on procedural proof languages, scripts, and rely on LCF tacticals as the primary tool for tactics composition. In this paper we discuss how these ingredients do not interact well with user interfaces based on the same interaction paradigm of Proof General (the de facto standard in this field), identifying in the coarse-grainedness of tactical evaluation the key problem. We propose Tinycals as an alternative to a subset of LCF tacticals, showing that the user does not experience the same problem if tacticals are evaluated in a more fine-grained manner. We present the formal operational semantics of Tinycals as well as their implementation in the Matita proof assistant.

Break (10:30‑11:00)

Session 2 (11:00‑12:00)

11:00‑11:30

Cezary Kaliszyk (Radboud University Nijmegen) Web Interfaces for Proof Assistants This article describes an architecture for creating responsive web interfaces for proof assistants. The architecture combines current web development technologies with the functionality of local prover interfaces, to create an interface that is available completely within a web browser, but resembles and behaves like a local one. Security, availability and efficiency issues of the proposed solution are described. A prototype implementation of a web interface for the Coq proof assistant created according to our architecture is presented. Access to the prototype is available on http://hair-dryer.cs.ru.nl:1024/.

11:30‑12:00

Marc Wagner (Saarland University, Germany) Serge Autexier (Saarland University, Germany) Christoph Benzmüller (Saarland University, Germany) PLATO: A Mediator between Text-Editors and Proof Assistance Systems We present a generic mediator, called PLATO, between text editors and proof assistants. PLATO aims at integrated support for the development, publication, formalization, and verification of mathematical documents in a natural way as possible: The user authors his mathematical documents with a scientific WYSIWYG text editor in the informal language he is used to, that is a mixture of natural language and formulas. These documents are then semantically annotated preserving the textual structure by using the flexible, parameterized proof language which we present. From this informal semantic representation PLATO automatically generates the corresponding formal representation for a proof assistant, in our case OMEGA. The primary task of PLATO is the maintenance of consistent formal and informal representations during the interactive development of the document.

Lunch break (12:30‑14:00)

Session 3 (14:00‑15:30)

14:00‑14:30	Anne Mulhern (University of Wisconsin-Madison) Charles Fischer (University of Wisconsin-Madison) Ben Liblit (University of Wisconsin-Madison) Tool Support for Proof Engineering Modern integrated development environments (IDEs) provide programmers with a variety of sophisticated tools for program visualization and manipulation. These tools assist the programmer in understanding legacy code and making coordinated changes across large parts of a program. Similar tools would assist proof developers in understanding and manipulating the increasingly larger proofs that are being developed. In this paper we propose some tools and techniques developed for software engineering that we believe would be equally applicable in proof engineering.
14:30‑15:00	Josef Urban (Charles University) Grzegorz Bancerek (Bialystok Technical University) Presenting and Explaining Mizar The Mizar proof language has both many human-friendly presentation features, and also firm semantical level allowing rigorous proof checking. Both the presentation features and the semantics are important for users, and an ideal Mizar presentation should be both human-friendly (i.e. very close to textbook presentations), and also allowing fast access to the detailed semantics and detailed proof explanations. This poses several questions, problems and choices when presenting original Mizar texts, presenting results of semantic queries over the Mizar library, and also when presenting texts produced directly on the semantical level, e.g. by automated theorem provers. This paper discusses solutions to these problems, and particularly implements an initial system for presenting detailed explanations of atomic Mizar inferences. This is done by the cooperation of the Mizar XML presentation tools, of the MML Query system, and of automated theorem provers working on the MPTP semantic translation of Mizar.
15:00‑15:30	Steven Trac (University of Miami) Yury Puzis (University of Miami) Geoff Sutcliffe (University of Miami) An Interactive Derivation Viewer This work describes the Interactive Derivation Viewer (IDV) tool for graphical rendering of derivations that are written in the TPTP language. IDV provides an interactive interface that allows the user to quickly view various features of the derivation. A particularly novel feature of IDV is its ability to provide a synopsis of a derivation by identifying interesting lemmas within a derivation, and hiding less interesting intermediate formulae. IDV is deployed online as part of the SystemOnTPTP interface, thus providing ready access via any web browser.

Break (15:30‑16:00)

Session 4 (16:00‑17:00)

16:00‑16:30

Peter C. Dillinger (Georgia Institute of Technology) Panagiotis Manolios (Georgia Tech) Daron Vroon (Georgia Institute of Technology, College of Computing) J Strother Moore (University of Texas at Austin) ACL2s: "The ACL2 Sedan" ACL2 is the latest inception of the Boyer-Moore theorem prover, the 2005 recipient of the ACM Software System Award. In the hands of experts it feels like a finely tuned race car, and it has been used to prove some of the most complex theorems ever proved about commercially designed systems. Unfortunately, ACL2 has a steep learning curve. Thus, novices tend have a very different experience: they crash and burn. As part of a project to make ACL2 and formal reasoning safe for the masses, we have developed ACL2s, the ACL2 sedan. ACL2s includes many features for streamlining the learning process that are not found in ACL2. In general, the goal is to develop a tool that is ``self-teaching,'' i.e., it should be possible for an undergraduate to sit down and play with it and learn how to program in ACL2 and how to reason about the programs she writes.

16:30‑17:00

Louise Abigail Dennis (University of Nottingham) Enhancing Theorem Prover Interfaces with Program Slice Information This paper proposes an extension to theorem proving interfaces for use with proof-directed debugging and other disproof-based applications. The extension is based around tracking a user-identified set of rules to create an informative program slice. Information is collected based on the involvement of these rules in both successful and unsuccessful proof branches. This provides a heuristic score for making judgements about the correctness of any rule. A simple mechanism for syntax highlighting based on such information is proposed and a small case study presented illustrating its operation. No implementation of these ideas yet exists.

Session 5: Discussion, Demos, Business Meeting (17:00‑18:00)