Providing a formal linkage between MDG and HOL