UTP2: Higher-Order Equational Reasoning by Pointing

Andrew Butterfield
(Trinity College Dublin)

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?

In Christoph Benzmüller and Bruno Woltzenlogel Paleo: Proceedings Eleventh Workshop on User Interfaces for Theorem Provers (UITP 2014), Vienna, Austria, 17th July 2014, Electronic Proceedings in Theoretical Computer Science 167, pp. 14–22.
Published: 29th October 2014.

ArXived at: https://dx.doi.org/10.4204/EPTCS.167.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org