dc.contributor.author | BUTTERFIELD, ANDREW | en |
dc.contributor.editor | Christoph Benzmüller and Bruno Woltzenlogel Paleo | en |
dc.date.accessioned | 2014-10-14T10:11:08Z | |
dc.date.available | 2014-10-14T10:11:08Z | |
dc.date.created | 17th July 2014 | en |
dc.date.issued | 2014 | en |
dc.date.submitted | 2014 | en |
dc.identifier.citation | 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 - 22 | en |
dc.identifier.other | Y | en |
dc.identifier.uri | http://hdl.handle.net/2262/71489 | |
dc.description | PUBLISHED | en |
dc.description | Vienna | en |
dc.description.abstract | 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? | en |
dc.format.extent | 14 | en |
dc.format.extent | 22 | en |
dc.language.iso | en | en |
dc.relation.ispartofseries | 167 | en |
dc.rights | Y | en |
dc.subject | Computer Science | en |
dc.title | UTP2: Higher-Order Equational Reasoning by Pointing | en |
dc.title.alternative | Electronic Proceedings in Theoretical Computer Science | en |
dc.title.alternative | Proceedings Eleventh Workshop on User Interfaces for Theorem Provers | en |
dc.type | Conference Paper | en |
dc.type.supercollection | scholarly_publications | en |
dc.type.supercollection | refereed_publications | en |
dc.identifier.peoplefinderurl | http://people.tcd.ie/butrfeld | en |
dc.identifier.rssinternalid | 97220 | en |
dc.rights.ecaccessrights | openAccess | |
dc.subject.TCDTag | Computer Software | en |
dc.contributor.sponsor | Science Foundation Ireland (SFI) | en |