Technical reports
Programming combinations of deduction and BDD-based symbolic calculation
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} }