Technical reports

Combining the Hol98 proof assistant with the BuDDy BDD package

Mike Gordon, Ken Friis Larsen

December 1999, 71 pages

Abstract

Theorem provers descended from LCF allow their users to write complex proof tools with high assurance that false theorems will not be proved. This report describes an experimental system that extends the LCF approach to enable combinations of deduction and BDD-based symbolic calculation to be programmed with a similar assurance. The deduction is supplied by the Hol98 system and the BDD algorithms by Jørn Lind-Nielsen’s BuDDy package.

The main idea is to provide LCF-style support to a set of inference rules for judgements ρ t ↦ b, where ρ is an order-inducing map from HOL variables to BDD variables, t is a HOL term and b is a BDD. A single oracle rule allows a HOL theorem ⊢ t to be deduced from ρ t ↦ TRUE.

This report is intended to serve as documentation for the Hol98 library HolBddLib. It is partly an exposition of standard results, partly tutorial and partly an account of research in combining deduction and symbolic state enumeration.

Full text

Only available on paper (could be scanned on request).

BibTeX record

@TechReport{UCAM-CL-TR-481,
  author =	 {Gordon, Mike and Larsen, Ken Friis},
  title = 	 {{Combining the Hol98 proof assistant with the BuDDy BDD
         	   package}},
  year = 	 1999,
  month = 	 dec,
  institution =  {University of Cambridge, Computer Laboratory},
  address =	 {15 JJ Thomson Avenue, Cambridge CB3 0FD, United Kingdom,
          	  phone +44 1223 763500},
  doi = 	 {10.48456/tr-481},
  number = 	 {UCAM-CL-TR-481}
}