BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Big Proof Agenda for Mechanizing Mathematical Discourse - Nata
 rajan Shankar (SRI International)
DTSTART:20170626T100000Z
DTEND:20170626T110000Z
UID:TALK73056@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:We are creating and using mathematical knowledge at a rapidly<
 br>increasing rate.&nbsp\; This growth creates the<br>need for automation 
 in<br>building and indexing formal mathematical&nbsp\;<br><br>knowledge<br
 >bases.&nbsp\; Automated proof technologies such<br>as theorem&nbsp\;provi
 ng\,<br>satisfiability solving\, and model checking are increasingly<br>be
 ing used for formalizing the behavior of computer&nbsp\;<br><br>hardware a
 nd<br>software systems\, constructing large libraries&nbsp\; of&nbsp\;form
 alized<br>mathematics\, and solving open problems.&nbsp\;<br>We outline&nb
 sp\; an agenda for<br>the Big Proof programme toward pragmatic foundations
 <br>and practical technologies that can assist pure and&nbsp\;applied<br>m
 athematicians solve large problems individually and&nbsp\;collaboratively.
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR