Trots sin tidiga död är H. känd för betydande pionjärarbeten i bevisteori. Ett av hans grundläggande resultat, H:s teorem, sammanbinder predikatlogik och satslogik och har viktiga tillämpningar även inom automatisk bevisföring. Det säger att en formel i prenex normalform är predikatlogiskt sann om och endast om en ändlig disjunktion