UTP2: Higher-Order Equational Reasoning by Pointing
This work addresses usability for researchers in formal methods, but it is incremental as it builds on existing frameworks without major breakthroughs.
The authors tackled the challenge of matching hand-written proof styles in the Unifying Theories of Programming framework by developing UTP2, a prototype theorem prover with a point-and-click user interface, contrasting it with command-line approaches.
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?