UTP2: Higher-Order Equational Reasoning by Pointing
Logic in Computer Science
2014-10-31 v1 Human-Computer Interaction
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?
Keywords
Cite
@article{arxiv.1410.8216,
title = {UTP2: Higher-Order Equational Reasoning by Pointing},
author = {Andrew Butterfield},
journal= {arXiv preprint arXiv:1410.8216},
year = {2014}
}
Comments
In Proceedings UITP 2014, arXiv:1410.7850