Dear all: I am a new learner of HOL , and I am also a researcher on hardware verification.
After learning HOL and COQ, and according to my experience in hardware verification, I get a feeling that : most, if not all, hardware verification problem can be solved with a framework similar to model checking, which generate CNF and call SAT/SMT solver. And it seems that almost all papers about coq and how appears in software language that reason about higher order logic. Is this correct? ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
