Technical reports
Proof by pointing
Yves Bertot, Gilles Kahn, Laurent Théry
October 1993, 27 pages
DOI: 10.48456/tr-313
Abstract
A number of very powerful and elegant computer programs to assist in making formal proofs have been developed. While these systems incorporate ever more sophisticated tactics, proofs that can be carried out without any user directions are the exception. In this paper we present a principle called proof by pointing that allows the user to guide the proof process using the mouse in the user-interface. This idea is widely applicable and has been implemented by the authors in user-interfaces for several proof development systems.
Full text
PDF (1.7 MB)
BibTeX record
@TechReport{UCAM-CL-TR-313, author = {Bertot, Yves and Kahn, Gilles and Th{\'e}ry, Laurent}, title = {{Proof by pointing}}, year = 1993, month = oct, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-313.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-313}, number = {UCAM-CL-TR-313} }