An automatic proof-generating translation from higher-order to first-order logic : with applications to linking HOL4 and ACL2

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]

Abstract

Abstract is missing.