|
Published: 29th October 2014 DOI: 10.4204/EPTCS.167 ISSN: 2075-2180 |
| Preface Christoph Benzmüller and Bruno Woltzenlogel Paleo | |
| Invited Presentation: The TPTP Process Instruction Language, with Applications Geoff Sutcliffe | 1 |
| Invited Presentation: Asynchronous processing of formal documents in Coq Enrico Tassi | 2 |
| How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of Interactive Theorem Provers Bernhard Beckert, Sarah Grebing and Florian Böhl | 4 |
| UTP2: Higher-Order Equational Reasoning by Pointing Andrew Butterfield | 14 |
| Tinker, tailor, solver, proof Gudmund Grov, Aleks Kissinger and Yuhui Lin | 23 |
| Advanced Proof Viewing in ProofTool Tomer Libal, Martin Riener and Mikheil Rukhaia | 35 |
| A Logic-Independent IDE Florian Rabe | 48 |
| The Certification Problem Format Christian Sternagel and René Thiemann | 61 |
| PIDE for Asynchronous Interaction with Coq Carst Tankink | 73 |
| System description: Isabelle/jEdit in 2014 Makarius Wenzel | 84 |
The UITP workshop series provides a forum for researchers interested in discussing human interaction with logic-based systems in general, including automated deduction tools and interactive proof assistants. The workshop welcomes papers aiming at designing, developing and evaluating user interfaces for such systems.
This volume contains the proceedings of the 11th International Workshop on User Interfaces for Theorem Provers (UITP 2014), held on the 17th of July 2014 during the Vienna Summer of Logic, in Austria. Ten papers were submitted. Each paper was reviewed by at least three referees, and following an online discussion, eight research papers were selected to be published in the proceedings and to be presented at the workshop. The program also included invited talks given by Geoff Sutcliffe (University of Miami), who presented "The TPTP Process Instruction Language, with Applications", and Enrico Tassi (INRIA), who addressed "Asynchronous Processing of Formal Documents in Coq".
We are grateful to the invited speakers and thankful to all participants of the UITP 2014 Workshop, especially to the authors for their submissions and to the members of the Program Committee of UITP 2014 for their professional work in the review process. We also would like to thank the Workshop Chairs and the Organizing Committee of the Vienna Summer of Logic (VSL 2014) for the smooth organization and for providing the great environment to which UITP was affiliated.
September 2014, Berlin and Vienna
Christoph Benzmüller
Department of Mathematics and Computer Science
Freie Universität Berlin
Arnimallee 7, 14195 Berlin, Germany
E-mail: c.benzmueller@fu-berlin.de
Bruno Woltzenlogel Paleo
Vienna University of Technology
Favoritenstraße 9, 1040 Wien, Austria
E-mail: bruno@logic.at
Most input languages for ATP systems, including the existing TPTP logical languages, are designed primarily to write the logical formulae that are input to and output from ATP systems' reasoning processes. There is minimal or no support for controlling the processing of the logical formulae: tasks such as incrementally adding and deleting formulae, controlling reasoning processes, and interacting with non-logical data. The TPTP Process Instruction (TPI) language augments the existing and well-known logical TPTP language forms with command and control instructions for manipulating logical formulae in the context of ATP systems. The TPI language makes it easy(er) for ATP users to specify their problems, process the logical formulae, and report results, in a fully automatic way. Two interpreters for the TPI language have been implemented, and have been productively used in several applications.
In recent years Interactive Theorem Provers (ITPs) have been successfully adopted to give an ultimate degree of reliability both to complex software systems, like the L4 microkernel and the CompCert C compiler, and to mathematical theorems, like the Odd Order Theorem. These large formalization projects have pushed interactive provers beyond their limits highlighting their deficiencies and opening for new challenges. The most compelling new requirement is reactivity: how long does it take the system to react to a user change and give him feedback. For example if one takes the full proof of the Odd Order Theorem [1] and makes a change, even trivial, in the first file and asks the prover any kind of feedback on the last file he has to wait approximatively 2 hours. Better reactivity can surely be achieved by faster processing of the formal documents, even more by doing it in a smarter way: giving precedence to the tasks the user is really interested in and postponing the others. In the light of that it is clear that the design of interactive provers needs to adapt to these new demands, and that this has to happen in conjunction with their user interfaces.
In the context of Paral-ITP project (ANR-11-INSE-001) the way Coq processes a formal document has been completely redesigned from the ground up, with the aim of allowing better reactivity, faster re- compilation and finally pave the way to modern user interfaces [3]. The seminal work of Wenzel [5, 6] in parallelizing the Isabelle system has been of great inspiration for this work.
This talk describes the new design of Coq and reports on the implementation that was undertaken during the last one and a half year. The aim is to give system developers an overview of the design choices that are crucial to obtain a reactive prover. In particular we discuss the following topics: 1) asynchronous interaction model, 2) formal document representation, 3) asynchronous proofs, 4) parallel execution in OCaml, 5) meta data collection.
The first requirement for having a more reactive prover is to not impose an eager execution of commands. The Read Eval Print Loop on top of which most user interfaces are built imposes such constraint. For example the prover must tell the user interface if a command fails or succeeds immediately: the prover is not given a second chance to report any feedback. If all commands have to be executed eagerly it is then impossible to postpone uninteresting tasks. The natural solution to this problem is to adopt an asynchronous interaction loop, as originally proposed by Wenzel. Commands sent to the prover and responses set to the user interface are equipped with unique identifiers. Responses are not expected to come in any precise order: the identifiers enable the user interface to make sense of the responses and to report feedback on the text they refer to.
Once the prover is not forced to produce an answer immediately a vast panel of possible optimizations is available. In our opinion the most interesting one is the static analysis of the document. In particular the system can represent it as a Direct Acyclic Graph (DAG) where nodes are system states and edges carry the tasks one has to perform in order to compute a state. On that representation it is easy to take scheduling decisions: for instance independent paths from one node to another can be performed in parallel. A requirement for that is that the language in which the formal document is written has a sufficiently clear semantics. For example the subdivision of a document into separate lemmas can help to identify independent proofs. But for this to work the beginning/ending of proofs must be clearly delimited. Branches in the DAG also identify failures/recovery points. A broken proof of a statement does not necessarily make the following part of the document invalid: if one fixes such proof (without changing the statement) then there is no need to recheck what follows.
The logical environment of a prover like Coq contains the statement and the proof evidence of theorems. A theorem enters the logical environment only if its proof evidence has been checked. When the checking of proofs is executed out of order this condition has to be relaxed. Wenzel introduced the concept of proof promise [4] in the core logic of Isabelle for this precise purpose. Another viable option is to rely on the semantics of the underlying programming language: the data type for the proof evidence is replaced by a lazy (and pure) computation that, when executed, produces the proof evidence and checks its correctness. Finally a logical environment is said to be sound only if all the lazy computations it contains have been evaluated.
To take advantage of multi core microprocessors one can process inde- pendent tasks in parallel. Coq is written in the OCaml programming language that leaves no option but splitting the work among separate processes. While this imposes a clean message passing discipline, one has to design a mechanism to efficiently send to a worker process the relevant bits of the system state. Trimming down the system state can be particularly difficult if the state of the prover is unstructured and non first class, as in the case of Coq. The ephemerons [2] finalization mechanism was successfully employed as a solution for that problem. The data one wants to trim down is not stored directly in the system state but represented by its ephemeron access key. When the system state is marshalled and sent over the wire, the unwanted data is not sent along with its corresponding ephemeron key since it lives outside the marshalled object. Finally, when an ephemeron key becomes unreferenced its corresponding data is eventually collected by the OCaml runtime, as if such data was equally unreferenced.
When multiple workers are checking independent parts of the same document the feedback each worker produces needs to reach the user interface. In our design the master process acts as a proxy and provides a mono directional bus on which workers write.