Department of Computer Science and Technology

Technical reports

Programming combinations of deduction and BDD-based symbolic calculation

Mike Gordon

December 1999, 24 pages

DOI: 10.48456/tr-480

Abstract

Theorem provers descended from LCF allow their users to write complex proof tools that provide high assurance that false theorems will not be proved. This paper describes some experiments in extending the ‘LCF approach’ to enable BDD-based symbolic algorithms to be programmed with a similar assurance. The deduction is supplied by the HOL system and the BDD algorithms by the BuDDy package.

Full text

PDF (1.7 MB)

BibTeX record

@TechReport{UCAM-CL-TR-480,
  author =	 {Gordon, Mike},
  title = 	 {{Programming combinations of deduction and BDD-based
         	   symbolic calculation}},
  year = 	 1999,
  month = 	 dec,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-480.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-480},
  number = 	 {UCAM-CL-TR-480}
}