Interactive Theorem Proving in Industry (Intel speaker)

http://events.inf.ed.ac.uk/Milner2012/J_Harrison-html5-mp4.htmlThis talk was part of the Milner symposium.

This talk mentions the idea of proving computer algebra

results. He notes that some classes of problems that can

be checked easily (aka have a certificate) exist.

For instance, factorization problems can easily be checked

by expanding the factorization back to the input.

Indefinite integration can be checked by differentiation.

But definite integration is harder and there is no obvious

way to produce a certificate.

He conjectures that there may be an NP-like class for

computer algebra where you can't check in polynomial time.

Altogether an interesting talk.

Tim

_______________________________________________

Axiom-developer mailing list

[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer