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. 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. 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. 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. The third round of the Kurt Gödel Research Prize Fellowships Program, under the title: Connecting Foundations and Technology, aims at supporting young scholars in early stages of their academic careers by offering highest fellowships in history of logic, kindly supported by the John Templeton Foundation. Young scholars being less or exactly 40 years old at the time of the commencement of the Vienna Summer of Logic (July 9, 2014) will be awarded one fellowship award in the amount of EUR 100,000, in each of the following categories:

• Logical Foundations of Mathematics,
• Logical Foundations of Computer Science, and
• Logical Foundations of Artificial Intelligence

The following three Boards of Jurors were in charge of choosing the winners:

• Logical Foundations of Mathematics: Jan Krajíček, Angus Macintyre, and Dana Scott (Chair).
• Logical Foundations of Computer Science: Franz Baader, Johann Makowsky, and Wolfgang Thomas (Chair).
• Logical Foundations of Artificial Intelligence: Luigia Carlucci Aiello, Georg Gottlob (Chair), and Bernhard Nebel.

http://fellowship.logic.at/

ABSTRACT. The aim of the FLoC Olympic Games is to start a tradition in the spirit of the ancient Olympic Games, a Panhellenic sport festival held every four years in the sanctuary of Olympia in Greece, this time in the scientific community of computational logic. Every four years, as part of the Federated Logic Conference, the Games will gather together all the challenging disciplines from a variety of computational logic in the form of the solver competitions.

At the Award Ceremonies, the competition organizers will have the opportunity to present their competitions to the public and give away special prizes, the prestigious Kurt Gödel medals, to their successful competitors. This reinforces the main goal of the FLoC Olympic Games, that is, to facilitate the visibility of the competitions associated with the conferences and workshops of the Federated Logic Conference during the Vienna Summer of Logic.

This award ceremony will host the

• 3rd Confluence Competition (CoCo 2014);
• Configurable SAT Solver Challenge (CSSC 2014);
• Ninth Max-SAT Evaluation (Max-SAT 2014);
• QBF Gallery 2014; and
• SAT Competition 2014 (SAT-COMP 2014).

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. The following new PIDE concepts are explained: asynchronous print functions and document overlays, syntactic and semantic completion, editor navigation, management of auxiliary files within the document-model.

See also Isabelle2014-RC0, which is the same pre-release snapshot that will be used in the Isabelle tutorial.

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 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?