Technical reports
Tactics and tacticals in Cambridge LCF
July 1983, 26 pages
DOI: 10.48456/tr-39
Abstract
The tactics and tacticals of Cambridge LCF are described. Tactics reason about logical connectives, substitution and rewriting; tacticals combine tactics into more powerful tactics. LCF’s package for managing an interactive proof is discussed. This manages the subgoal tree, presenting the user with unsolved goals and assembling the final proof.
While primarily a reference manual, the paper contains a brief introduction to goal-directed proof. An example shows typical use of the tactics and subgoal package.
Full text
PDF (0.9 MB)
BibTeX record
@TechReport{UCAM-CL-TR-39, author = {Paulson, Lawrence}, title = {{Tactics and tacticals in Cambridge LCF}}, year = 1983, month = jul, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-39.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-39}, number = {UCAM-CL-TR-39} }