Computer Laboratory

Technical reports

Efficiency in a fully-expansive theorem prover

Richard John Boulton

May 1994, 126 pages

This technical report is based on a dissertation submitted December 1993 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Churchill College.

Abstract

The HOL system is a fully-expansive theorem prover: Proofs generated in the system are composed of applications of the primitive inference rules of the underlying logic. This has two main advantages. First, the soundness of the system depends only on the implementations of the primitive rules. Second, users can be given the freedom to write their own proof procedures without the risk of making the system unsound. A full functional programming language is provided for this purpose. The disadvantage with the approach is that performance is compromised. This is partly due to the inherent cost of fully expanding a proof but, as demonstrated in this thesis, much of the observed inefficiency is due to the way the derived proof procedures are written.

This thesis seeks to identify sources of non-inherent inefficiency in the HOL system and proposes some general-purpose and some specialised techniques for eliminating it. One area that seems to be particularly amenable to optimisation is equational reasoning. This is significant because equational reasoning constitutes large portions of many proofs. A number of techniques are proposed that transparently optimise equational reasoning. Existing programs in the HOL system require little or no modification to work faster.

The other major contribution of this thesis is a framework in which part of the computation involved in HOL proofs can be postponed. This enables users to make better use of their time. The technique exploits a form of lazy evaluation. The critical feature is the separation of the code that generates the structure of a theorem from the code that justifies it logically. Delaying the justification allows some non-local optimisations to be performed in equational reasoning. None of the techniques sacrifice the security of the fully-expansive approach.

A decision procedure for a subset of the theory of linear arithmetic is used to illustrate many of the techniques. Decision procedures for this theory are commonplace in theorem provers due to the importance of arithmetic reasoning. The techniques described in the thesis have been implemented and execution times are given. The implementation of the arithmetic procedure is a major contribution in itself. For the first time, users of the HOL system are able to prove many arithmetic lemmas automatically in a practical amount of time (typically a second or two).

The applicability of the techniques to other fully-expansive theorem provers and possible extensions of the ideas are considered.

Full text

DVI (0.2 MB)

BibTeX record

@TechReport{UCAM-CL-TR-337,
  author =	 {Boulton, Richard John},
  title = 	 {{Efficiency in a fully-expansive theorem prover}},
  year = 	 1994,
  month = 	 may,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-337.dvi.gz},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-337}
}