简介：Inthispaper,weprovideanecessaryinfrastructuretodefineanabstractstateexplorationintheHOLtheoremprover.OurinfrastructureisbasedonadeepembeddingoftheMultiwayDecisionGraphs(MDGs)theoryinHOL.MDGsgeneralizeReducedOrderedBinaryDecisionDiagrams(ROBDDs)torepresentandmanipulateasubsetoffirst-orderlogicformulae.TheMDGsembeddingisbasedonthelogicalformulationofanMDGasDirectedFormulae(DF).Then,theMDGsoperationsaredefinedandthecorrectnessproofofeachoperationisprovided.TheMDGreachabilityalgorithmisthendefinedasaconversionthatusesourMDGtheorywithinHOL.Finally,asetofexperimentationsoverbenchmarkcircuitshasbeenconductedtoensuretheapplicabilityandtomeasuretheperformanceofourapproach.