UTP2: Higher-Order Equational Reasoning by Pointing
![Thumbnail](/xmlui/themes/Mirage2/images/white_rectangle.jpeg)
File Type:
PDFItem Type:
Conference PaperDate:
2014Author:
Access:
openAccessCitation:
Andrew Butterfield, UTP2: Higher-Order Equational Reasoning by Pointing, Electronic Proceedings in Theoretical Computer Science, Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, Vienna, 17th July 2014, Christoph Benzmüller and Bruno Woltzenlogel Paleo, 167, 2014, 14 - 22Abstract:
We describe a prototype theorem prover,
U.(TP)2, 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?
Sponsor
Grant Number
Science Foundation Ireland (SFI)
Author's Homepage:
http://people.tcd.ie/butrfeldDescription:
PUBLISHEDVienna
Author: BUTTERFIELD, ANDREW
Other Titles:
Electronic Proceedings in Theoretical Computer ScienceProceedings Eleventh Workshop on User Interfaces for Theorem Provers
Type of material:
Conference PaperCollections
Series/Report no:
167Availability:
Full text availableKeywords:
Computer ScienceSubject (TCD):
Computer SoftwareMetadata
Show full item recordLicences: