UTP2: Higher-Order Equational Reasoning by Pointing

TL;DR

UTP2 is a prototype theorem prover designed for higher-order equational reasoning within the Unifying Theories of Programming framework, emphasizing an intuitive point-and-click user interface over traditional command-line tools.

Contribution

This work introduces a novel user interface for a theorem prover that combines the advantages of graphical interaction with formal equational reasoning in a second-order logic setting.

Findings

Prototype developed with a point-and-click interface

Focus on matching hand-written proof style

Contrast with command-line theorem provers

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?