James Reynolds. An automatic proof-generating translation from higher-order to first-order logic : with applications to linking HOL4 and ACL2. PhD thesis, University of Cambridge, UK, 2009. [doi]
No references recorded for this publication.
No citations of this publication recorded.