UITP 2014 PROCEEDINGS: PAPERS WITH ABSTRACTS

ABSTRACT. We describe a prototype theorem prover, \UTP2, developed to match the style of hand-written proof work in the Unifying Theories of Programming semantical framework. This is based on alphabetised predicates in a 2nd-order logic, with a strong emphasis on equational reasoning. We present here an overview of the user-interface of this prover, which was developed from the outset using a point-and-click approach. We contrast this with the command-line paradigm that continues to dominate the mainstream theorem provers, and raises the question: can we have the best of both worlds?

ABSTRACT. In recent years the effectiveness of interactive theorem provers has increased to an extend that the bottleneck in the interactive process shifted to efficiency: while in principle large and complex theorems are provable (effectiveness), it takes a lot of effort for the user interacting with the system (lack of efficiency). We conducted focus groups to evaluate the usability of Isabelle/HOL and the KeY system with two goals: (a) detect usability issues in the interaction between interactive theorem provers and their user, and (b) analyze how evaluation methods commonly used in the area of human-computer interaction, such as focus groups and co-operative evaluation, are applicable to the specific field of interactive theorem proving(ITP).

In this paper, we report on our experience using the evaluation method focus groups and how we adapted this method to ITP. We describe our results and conclusions mainly on the ``meta-level,'' i.e., we focus on the impact that specific characteristics of ITPs have on the setup and the results of focus groups. On the concrete level, we briefly summarise insights into the usability of the ITPs used in our case study.

ABSTRACT. We introduce Tinker, a tool for designing an evaluating proof strategies based on proof-strategy graphs, a formalism previously introduced by the authors. We represent proof strategies as open-graphs, which are directed graphs with additional input/output edges. Tactics appear as nodes in a graph, and can be `piped' together by adding edges between them. Goals are added to the input edges of such a graph, and flow through the graph as the strategy is evaluated. Properties of the edges ensure that only the right `type' of goals are accepted. In this paper, we detail the Tinker tool and show how it can be integrated with two different theorem provers: Isabelle and ProofPower.

ABSTRACT. Sequent calculus is widely used for formalizing proofs. However, understanding the proofs of even simple mathematical arguments soon becomes impossible. Graphical user interfaces help in this matter, but most stick with Gentzen's original notation. This paper tries to catch up with recent developments in tree visualization and proposes the Sunburst Tree layout as a complement to the traditional tree structure. It constructs inferences as concentric circle arcs around the root inference, allowing the user to investigate the proof's structural content. We further describe the integration into PROOFTOOL and the interaction with the Gentzen layout.

ABSTRACT. Interactive deduction systems are becoming increasingly powerful and practical. While design has historically focused on questions such as the choice of logic or the strength of the prover, modern systems must additionally satisfy practical requirements such as good IDEs or easily-searchable libraries. We hypothesize that many such practical requirements can be solved independently of the specific logic or prover, and that doing so will enable a fruitful separation of concerns between logic/prover and user interface developers.

To that end, we design and implement a logic-independent IDE-style user interface, which we base on the jEdit editor and the MMT language. jEdit is a full-fledged and extensible text editor, and MMT is a logic-independent representation format that already offers a variety of generic knowledge management services. Taken together, they let us realize strong user support at comparatively little cost: Example features of our IDE include hyperlinking, awareness of inferred information, library browsing, search, and change management.

ABSTRACT. We provide an overview of CPF, the certification problem format, and explain some design decisions. Whereas CPF was originally invented to combine three different formats for termination proofs into a single one, in the meanwhile proofs for several other properties of term rewrite systems are also expressible: like confluence, complexity, and completion. As a consequence, the format is already supported by several tools and certifiers. Its acceptance is also demonstrated in international competitions: the certified tracks of both the termination and the confluence competition utilized CPF as exchange format between automated tools and trusted certifiers.

ABSTRACT. This paper describes the initial progress towards integrating the Coq proof assistant with the PIDE architecture initially developed for Isabelle. The architecture is aimed at asynchronous, parallel interaction with proof assistants, and is tied in heavily with a plugin that allows the jEdit editor to work with Isabelle.

We have made some generalizations to the PIDE architecture to accommodate for more provers than just Isabelle, and adapted Coq to understand the core protocol: this delivered a working system in about two man-months.

ABSTRACT. This is an updated system description for Isabelle/jEdit, according to the state of the official release Isabelle2013-2 (December 2013) and the forthcoming release Isabelle2014 that is anticipated for Summer 2014.