Journal of Undergraduate Research
Keywords
BDD, binary decision diagrams, tautology checker, HOL, higher-order logic
College
Physical and Mathematical Sciences
Department
Computer Science
Abstract
As computer systems become an integral part of society, ensuring that systems perform correctly will become more important. Proofs of correctness based on formal logic are one approach to the correctness problem in computer system design. Unfortunately, these proofs are often large and difficult for industrial size projects. The Higher-Order Logic (HOL) [GM93) automated proof assistant helps manage the details and validate the accuracy of large proofs.
Recommended Citation
Jones, Michael
(2014)
"BDD BASED TAUTOLOGY CHECKER,"
Journal of Undergraduate Research: Vol. 2014:
Iss.
1, Article 1179.
Available at:
https://scholarsarchive.byu.edu/jur/vol2014/iss1/1179