Department of Computer Science and Technology

Technical reports

Tactics and tacticals in Cambridge LCF

Lawrence Paulson

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