University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > The Big Proof Agenda for Mechanizing Mathematical Discourse

The Big Proof Agenda for Mechanizing Mathematical Discourse

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact info@newton.ac.uk.

BPR - Big proof

We are creating and using mathematical knowledge at a rapidly increasing rate.  This growth creates the need for automation in building and indexing formal mathematical  knowledge bases.  Automated proof technologies such as theorem proving, satisfiability solving, and model checking are increasingly being used for formalizing the behavior of computer  hardware and software systems, constructing large libraries  of formalized mathematics, and solving open problems.  We outline  an agenda for the Big Proof programme toward pragmatic foundations and practical technologies that can assist pure and applied mathematicians solve large problems individually and collaboratively.



This talk is part of the Isaac Newton Institute Seminar Series series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity