Artwork

Content provided by The Thesis Review and Sean Welleck. All podcast content including episodes, graphics, and podcast descriptions are uploaded and provided directly by The Thesis Review and Sean Welleck or their podcast platform partner. If you believe someone is using your copyrighted work without your permission, you can follow the process outlined here https://ro.player.fm/legal.
Player FM - Aplicație Podcast
Treceți offline cu aplicația Player FM !

[20] Josef Urban - Deductive and Inductive Reasoning in Large Libraries of Formalized Mathematics

1:25:18
 
Distribuie
 

Manage episode 302418425 series 2982803
Content provided by The Thesis Review and Sean Welleck. All podcast content including episodes, graphics, and podcast descriptions are uploaded and provided directly by The Thesis Review and Sean Welleck or their podcast platform partner. If you believe someone is using your copyrighted work without your permission, you can follow the process outlined here https://ro.player.fm/legal.
Josef Urban is a Principal Researcher at the Czech Institute of Informatics, Robotics, and Cybernetics. His research focuses on artificial intelligence for large-scale computer-assisted reasoning. Josef's PhD thesis is titled "Exploring and Combining Deductive and Inductive Reasoning in Large Libraries of Formalized Mathematics", which he completed in 2004 at Charles University in Prague. We discuss his PhD work on the Mizar Problems for Theorem Proving, machine learning for premise selection, and how it evolved into his recent research. Episode notes: https://cs.nyu.edu/~welleck/episode20.html Follow the Thesis Review (@thesisreview) and Sean Welleck (@wellecks) on Twitter, and find out more info about the show at https://cs.nyu.edu/~welleck/podcast.html Support The Thesis Review at www.patreon.com/thesisreview or www.buymeacoffee.com/thesisreview
  continue reading

47 episoade

Artwork
iconDistribuie
 
Manage episode 302418425 series 2982803
Content provided by The Thesis Review and Sean Welleck. All podcast content including episodes, graphics, and podcast descriptions are uploaded and provided directly by The Thesis Review and Sean Welleck or their podcast platform partner. If you believe someone is using your copyrighted work without your permission, you can follow the process outlined here https://ro.player.fm/legal.
Josef Urban is a Principal Researcher at the Czech Institute of Informatics, Robotics, and Cybernetics. His research focuses on artificial intelligence for large-scale computer-assisted reasoning. Josef's PhD thesis is titled "Exploring and Combining Deductive and Inductive Reasoning in Large Libraries of Formalized Mathematics", which he completed in 2004 at Charles University in Prague. We discuss his PhD work on the Mizar Problems for Theorem Proving, machine learning for premise selection, and how it evolved into his recent research. Episode notes: https://cs.nyu.edu/~welleck/episode20.html Follow the Thesis Review (@thesisreview) and Sean Welleck (@wellecks) on Twitter, and find out more info about the show at https://cs.nyu.edu/~welleck/podcast.html Support The Thesis Review at www.patreon.com/thesisreview or www.buymeacoffee.com/thesisreview
  continue reading

47 episoade

Alle episoder

×
 
Loading …

Bun venit la Player FM!

Player FM scanează web-ul pentru podcast-uri de înaltă calitate pentru a vă putea bucura acum. Este cea mai bună aplicație pentru podcast și funcționează pe Android, iPhone și pe web. Înscrieți-vă pentru a sincroniza abonamentele pe toate dispozitivele.

 

Ghid rapid de referință