Technical reports

On efficiency in theorem provers which fully expand proofs into primitive inferences

Richard J. Boulton

February 1992, 23 pages

DOI: 10.48456/tr-248

Abstract

Theorem Provers which fully expand proofs into applications of primitive inference rules can be made highly secure, but have been criticized for being orders of magnitude slower than many other theorem provers. We argue that much of this relative inefficiency is due to the way proof procedures are typically written and not all is inherent in the way the systems work. We support this claim by considering a proof procedure for linear arithmetic. We show that straightforward techniques can be used to significantly cut down the computation required. An order of magnitude improvement in the performance is shown by an implementation of these techniques.

Full text

DVI (0.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-248,
  author =	 {Boulton, Richard J.},
  title = 	 {{On efficiency in theorem provers which fully expand proofs
         	   into primitive inferences}},
  year = 	 1992,
  month = 	 feb,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-248.dvi.gz},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-248},
  number = 	 {UCAM-CL-TR-248}
}