Department of Computer Science and Technology

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}
}