Hello everyone,
The paper "Formal verification of floating point trigonometric
functions" by John Harrison from TPHOLs'97 gives a formal proof of
sturm's theorem and how to apply it to find roots of a polynomial in
HOL. I am trying to find the accompanying formal development as the
proof (and use) of Sturm's theorem is of special interest to me.
I tried searching the HOL-Light repository at
https://github.com/jrh13/hol-light <https://github.com/jrh13/hol-light>
and the HOL4 sources but could not find any mention of sturm's theorem.
Does someone have a pointer to where I could find the sources of the
development?
Thank you and best regards,
Heiko
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
