July 13th, 2018. Oxford, UK. A FLoC 2018 workshop.
The User Interfaces for Theorem Provers workshop series (UITP) brings together researchers interested in designing, developing and evaluating interfaces for interactive proof systems, such as theorem provers, formal method 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 welcome participation and 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. Topics covered 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
- Visualisation of mathematical objects and proof
- System descriptions
UITP 2018 is a one-day workshop to be held on Friday, July 13th 2018, in Oxford, UK, as a FLoC 2018 workshop.
Here is the list of accepted papers for the workshop. The workshop will start at 9:00, and include a joint session with the Isabelle workshop. For the actual programme with times and locations, we refer you to the FLoC web pages.
- Jamie Vicary: Designing Globular: formal proofs as geometrical objects (Invited Talk)
- Tomer Libal: Interfacing
with a Prover using Focusing and Logic Programming
Interfacing with theorem provers is normally done by specifying a strategy. Such a strategy can be local, such as using tactics in interactive theorem provers, or global when using automatic ones. Focused proof calculi have a clear separation between the phases in the proof search which can be done fully automatically and those phases which require decision making. The inference rules of these proof calculi can be defined using logical formulas, such as implications. Logic programming languages allow for proof search over a database of such logical formulas and also support interaction with the user via input/output calls. In this paper we describe a possible process of writing an interactive proof assistant over a focused sequent calculus using the higher-order programming language lambda-prolog. We show that one can gain a high level of trust in the correctness of the prover, up to the correctness of an extremely small kernel. This process might allow one to obtain a fully functional proof assistant using a small amount of code and by using a clear process for arbitrary focused calculi.
- Jan Gorzny, Ezequiel Postan and Bruno Woltzenlogel
Paleo: Partial Regularization of First-Order
Resolution and superposition are common techniques which have seen widespread use with propositional and first-order logic in modern theorem provers. In these cases, resolution proof production is a key feature of such tools; however, the proofs that they produce are not necessarily as concise as possible. For propositional resolution proofs, there are a wide variety of proof compression techniques. There are fewer techniques for compressing first-order resolution proofs generated by automated theorem provers. This paper describes an approach to compressing first-order logic proofs based on lifting proof compression ideas used in propositional logic to first-order logic. One method for propositional proof compression is partial regularization, which removes an inference n when it is redundant in the sense that its pivot literal already occurs as the pivot of another inference in every path from n to the root of the proof. This paper describes the generalization of the partial-regularization algorithm RecyclePivotsWithIntersection  from propositional logic to first-order logic. An empirical evaluation of the generalized algorithm and its combinations with the previously lifted GreedyLinearFirstOrderLowerUnits algorithm is also presented.
- Sarah Grebing, An Thuy Tien Luong and Alexander
Weigl: Adding Text-Based Interaction to a
Direct-Manipulation Interface for Program Verification -- Lessons Learned
Interactive program verification is characterized by iterations of unfinished proof attempts. For proof construction, many interactive program verification systems offer either text-based interactions, in using a proof scripting language, or a form of direct-manipulation interaction. We have combined a direct-manipulation program verification system with a text-based interface to leverage the advantages of both interaction paradigms. To give the user more insight when scripting proofs we have adapted well-known interaction concepts from the field of software debugging. In this paper we contribute with experiences from combining the direct-manipulation interface of the interactive program verification system KeY with a text-based user interface to construct program verification proofs leveraging interaction concepts from the field of software-debugging for the proof process.
- Rustam Zhumagambetov and Mark Sterling: Automated Theorem Proving in a Chat Environment
We present a chat bot as an interface to the Coq proof assistant. It provides modern way of interaction with Coq across multiple devices. We emphasize that it runs on several platform, having not the same interface but similar, at the same time it employs features of particular device. Moreover it is also easy to run it on mobile devices with Android and iOS.
- Makarius Wenzel: Isabelle/PIDE after 10 years of development
The beginnings of the Isabelle Prover IDE framework (Isabelle/PIDE) go back to the year 2008. This is a report on the project after 10 years, with system descriptions for various PIDE front-ends, namely (1) Isabelle/jEdit, the main PIDE application and default Isabelle user-interface, (2) Isabelle/VSCode, an experimental application of the Language Server Protocol in Visual Studio Code (by Microsoft), and (3) a headless PIDE server with JSON protocol messages over TCP sockets.
- Steffen Frerix and Peter Koepke: Text-Orientated Formal Mathematics
The System for Automated Deduction (SAD) by Andrei Paskevich proof-checks texts written in nearly natural mathematical language, without explicit system commands or prover commands. Natural language features like soft typing by noun phrases guide efficient text processing and proof checking. We have implemented practical improvements of the checking algorithm and extensions of the input language, so that we are now able to process considerably longer and more complicated texts. These are immediately readable by mathematicians, as demonstrated by subsequent examples. This suggests an approach to formal mathematics through collections or libraries of texts in (a controlled) natural language.
Submitted papers should describe previously unpublished work (completed or in progress), and be at least 4 pages and at most 12 pages. We encourage concise and relevant papers. Submissions should be in PDF format, and typeset with the EPTCS LaTeX document class (which can be downloaded from http://style.eptcs.org/). Submission is via EasyChair (https://www.easychair.org/conferences/?conf=uitp2018).
All papers will be peer reviewed by members of the programme committee and selected by the organisers in accordance with the referee reports.
At least one author/presenter of accepted papers must attend the workshop and present the work.
- Submission deadline: 15.04.2018
- Acceptance notification: 15.05.2018
- Camera-ready copy: 25.05.2018
- Workshop: 13.07.2018
Authors will have the opportunity to incorporate feedback and insights gathered during the workshop to improve their accepted papers before publication in the post-proceedings in the Electronic Proceedings in Theoretical Computer Science (EPTCS).
- Mateja Jamnik, University of Cambridge, UK (co-Chair)
- Christoph Lüth, University of Bremen, Germany (co-Chair)
- Serge Autexier, DFKI Bremen, Germany
- David Aspinall, University of Edinburgh, UK
- Chris Benzmüller, Free University Berlin, Germany
- Yves Bertot, INRIA Sophia-Antipolis, France
- Maria Paola Bonacina, University of Verona, Italy
- Joachim Breitner, University of Pennsylvania, USA
- Ross Duncan, University of Strathclyde, UK
- Moa Johansson, Chalmers University, Sweden
- Zoltán Kovács, RISC, Austria
- Mohamed Yousri Mahmoud, University of Ottawa, Canada
- Michael Norrish, NICTA, Australia
- Andrei Paskevich, LRI, France
- Larry Paulson, University of Cambridge, UK
- Alison Pease, University of Dundee, UK
- Pedro Quaresma, University of Coimbra, Portugal
- Gem Stapleton (University of Brighton, UK)
- Christian Sternagel, University of Innsbruck, Austria
- Enrico Tassi, INRIA Sophia-Antipolis, France
- Laurent Théry, INRIA Sophia-Antipolis, France
- Makarius Wenzel, Sketis, Germany
- Wolfgang Windsteiger, RISC Linz, Austria
- Bruno Woltzenlogel Paleo, Technical University Vienna, Austria