UTP2: Higher-Order Equational Reasoning by Pointing

Autor:	Butterfield, Andrew
Rok vydání:	2014
Předmět:	Computer Science - Logic in Computer Science Computer Science - Human-Computer Interaction
Zdroj:	EPTCS 167, 2014, pp. 14-22
Druh dokumentu:	Working Paper
DOI:	10.4204/EPTCS.167.4
Popis:	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? Comment: In Proceedings UITP 2014, arXiv:1410.7850
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/1410.8216 Zobrazit plný text záznamu View this record from Arxiv