%0 Thesis %1 phd/ethos/Reynolds09 %A Reynolds, James %D 2009 %K %T An automatic proof-generating translation from higher-order to first-order logic : with applications to linking HOL4 and ACL2.

@phdthesis{phd/ethos/Reynolds09, added-at = {2023-12-14T16:48:22.000+0100}, author = {Reynolds, James}, biburl = {https://www.bibsonomy.org/bibtex/20c693cd6e889ed67de4313c2716d16d3/admin}, ee = {http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.611133}, interhash = {fd5daf5e24b549c8df03cb5b8b1378d7}, intrahash = {0c693cd6e889ed67de4313c2716d16d3}, keywords = {}, note = {British Library, EThOS}, school = {University of Cambridge, UK}, timestamp = {2023-12-14T16:48:22.000+0100}, title = {An automatic proof-generating translation from higher-order to first-order logic : with applications to linking HOL4 and ACL2.}, year = 2009 }