I don't personally know of anything about matrix multiplication in HOL, but hopefully someone else might... Even if there's nothing in HOL, perhaps is some theory in HOL Light or Isabelle/HOL that could be ported?
Same for LFSR and polynomials over finite fields. On Mon, Aug 11, 2014 at 9:41 AM, Robert Künnemann < [email protected]> wrote: > Hello everyone, > > I've got two questions: > > 1. Can anyone point me to a theory in HOL formalizing matrx multiplication? > > 2. I need to formalize a linear-feedback shift register. They are > usually expressed in finite field arithmetic as a polynomial mod 2. So > far I've only found a theory for polynomials over \mathbb{R}. Am I right > that modelling the LSFR via wordslib is the easiest way? > > Cheers, Robert > > -- > Robert Künnemann, Ph.D. > Security in Information Technology, TU Darmstadt > Mornewegstraße 30, Room 4.1.05, D64293 Darmstadt > Phone: +49 6151 16 75532 > > > > ------------------------------------------------------------------------------ > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info >
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
