|09:30||John Slaney |
Visualising Reasoning: What ATP can learn from CP
Tools for graphical representation of problems in automated deduction or of proof searches are rare and mostly primitive. By contrast, there is a more substantial history of work in the constraint programming community on information visualisation techniques for helping programmers and end users to understand problems, searches and solutions. Here we consider the extent to which concepts and tools from a constraint programming platform can be adapted for use with automatic theorem provers.
|10:30||Makarius Wenzel |
Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit
After several decades, most proof assistants are still centered around TTY-bound interaction in a tight read-eval-print loop. Even well-known Emacs modes for such provers follow this synchronous model based on single commands with immediate response, meaning that the editor waits for the prover after each command. There have been some attempts to re-implement prover interfaces in big IDE frameworks, while keeping the old interaction model. Can we do better than that?
Already 10 years ago, the Isabelle/Isar proof language has emphasized the idea of "proof document" (structured text) instead of "proof script" (sequence of commands), although the implementation was still emulating TTY interaction in order to be able to work with the existing Proof~General interface. After some recent reworking of Isabelle internals, in order to support parallel processing of theories and proofs, the original idea of structured document processing has surfaced again.
Isabelle versions from 2009 or later already provide some support for interactive proof documents with asynchronous checking, which awaits to be connected to a suitable editor framework or full-scale IDE. The remaining problem is how to do that systematically, without having to specify and implement complex protocols for prover interaction.
This is the point where we introduce the new Isabelle/Scala layer, which is meant to expose certain aspects of Isabelle/ML to the outside world. The Scala language (by Martin Odersky) is sufficiently close to ML in order to model well-known prover concepts conveniently, but Scala also runs on the JVM and can access existing Java libraries directly. By building more and more external system wrapping for Isabelle in Scala, we eventually reach the point where we can integrate the prover seamlessly into existing IDEs (say Netbeans).
To avoid getting side-tracked by IDE platform complexity, our current experiments are focused on jEdit, which is a powerful editor framework written in Java that can be easily extended by plugin modules. Our plugins are written again in Scala for our convenience, and to leverage the Scala actor library for parallel and interactive programming. Thanks to the Isabelle/Scala layer, the Isabelle/jEdit implementation is very small and simple. By enhancing GUI connectivity like that, we essentially provide a theorem prover for user-interfaces.
|11:00||Holger Gast |
Engineering the Prover Interface
Practical prover interfaces are sizeable pieces of software, whose construction and maintenance requires an extensive amount of effort and resources. This paper addresses the engineering aspects of such developments. Using non-functional properties as quality attributes for software, we discuss which properties are particularly relevant to prover interfaces and demonstrate, by the example of the \itp\ interface for Isabelle, how judicious architectural and design decisions lead to an interface software possessing these properties. By a comparison with other proposed interfaces, we argue that our considerations can be applied beyond the example project.
|11:30||Carst Tankink, Herman Geuvers and James McKinna |
Narrating Formal Proof (Work in Progress)
Building on existing work to proxy interaction with proof assistants, we have considered the problem of how to augment this data structure to support commentary on formal proof development. In this setting, we have studied extracting commentary from an online text by Pierce et al.
|12:00||Freek Wiedijk |
For interactive theorem provers a very desirable property is _consistency_: it should not be possible to prove false theorems. However, this is not enough: it also should not be possible to _think_ that a theorem has been proved that actually is false. More precisely: the user should be able to _know_ what it is that the interactive theorem prover is proving.
To make these issues concrete we introduce the notion of _Pollack-consistency_. This property is related to a system being able to correctly parse formulas that it printed itself. In current systems it happens regularly that this fails.
We argue that a good interactive theorem prover should be Pollack-consistent. We show with examples that many interactive theorem provers currently are _not_ Pollack-consistent. Finally we describe a simple approach for making a system Pollack-consistent, which only consists of a small modification to the printing code of the system.
|14:00||Tuan Minh Pham and Yves Bertot |
A combination of a dynamic geometry software with a proof assistant for interactive formal proofs
This paper presents an interface for geometry proving. It is a combination of a dynamic geometry software - Geogebra with a proof assistant - Coq. Thanks to feature of Geogebra, users can create and manipulate geometric construction, they discover conjectures and interactively built formal proofs with the support of Coq. Our system allows user to construct fully traditional proofs which is in the same style as the ones in high school. For each step of proving, we provide a set of applicable rules verified in Coq for users, we also provide tactics in Coq by which minor steps of reasoning are solved automatically.
|14:30||Vladimir Komendantsky, Alexander Konovalov and Steve Linton |
Interfacing Coq + SSReflect with GAP
We report on an extendable implementation of the communication interface connecting Coq proof assistant to the computational algebra system GAP using the Symbolic Computation Software Composability Protocol (SCSCP). It allows Coq to issue OpenMath requests to a local or remote GAP instances and represent server responses as Coq terms.
|15:30||Andrei Lapets and Assaf Kfoury |
A User-friendly Interface for a Lightweight Verification System
User-friendly interfaces can play an important role in bringing to a wider audience the benefits of a machine-readable representation of formal arguments. The ``aartifact" system is an easy-to-use lightweight verifier for formal arguments that involve logical and algebraic manipulations of common mathematical concepts. The system provides validation capabilities by utilizing a large database of propositions governing common mathematical concepts. The system's multi-faceted interactive user interface combines several approaches to friendly interface design: (1) a familiar and natural syntax based on existing conventions in mathematical practice, (2) a real-time keyword-based lookup mechanism for interactive, context-sensitive discovery of the syntactic idioms and semantic concepts found in the system's large database of propositions, and (3) immediate validation feedback in the form of reformatted raw input. The system's natural syntax and large database of propositions allow it to meet a user's expectations in the formal reasoning scenarios for which it is intended. The real-time keyword-based lookup mechanism and validation feedback allow the system to teach the user about its capabilities and limitations in an immediate, interactive, and context-aware manner.
|16:00||Laura Meikle and Jacques Fleuriot |
Integrating Systems around the User: Combining Isabelle, Maple, and QEPCAD in the Prover's Palette
We describe the Prover's Palette, a general, modular architecture for combining tools for formal verification, with the key differentiator that the integration emphasises the role of the user. A concrete implementation combining the theorem prover Isabelle with the computer algebra systems Maple and QEPCAD-B is then presented. This illustrates that the design principles of the Prover's Palette simplify tool integrations while enhancing the power and usability of theorem provers.