Artificial Intelligence and Theorem Proving
Jan 26, 2017
Speakers
Josef Urban
Speaker · 4 followers
About
Probereme některé metody umělé inteligence, jimiž se lze učit dokazovat hypotézy nad velkými formálními matematickými korpusy. Tyto metody zahrnují (I) techniky strojového učení, jež se z předchozích důkazů učí navrhovat lemmata co nejrelevantnější pro dokazování dalších hypotéz, (II) metody, které na základě popisů dřívějších důkazů řídí nízkoúrovňové algoritmy vyhledávání důkazů a (III) metody, jež samostatně vymýšlejí vhodné dokazovací strategie pro dané třídy problémů. Ukážu příklady systémů umělé inteligence zahrnujících kladnou zpětnou vazbu mezi indukcí a dedukcí, a předvedu výkonnost současných metod nad velkými knihovnami existujících dokazovacích asistentů, jako jsou Isabelle, Mizar a HOL. Nakonec se zmíním o nově vznikajících systémech umělé inteligence kombinujících techniky statistického větného rozboru neformálních matematických vět se silnými metodami dokazování vět. http://www.praguecomputerscience.cz/Probereme některé metody umělé inteligence, jimiž se lze učit dokazovat hypotézy nad velkými formálními matematickými korpusy. Tyto metody zahrnují (I) techniky strojového učení, jež se z předchozích důkazů učí navrhovat lemmata co nejrelevantnější pro dokazování dalších hypotéz, (II) metody, které na základě popisů dřívějších důkazů řídí nízkoúrovňové algoritmy vyhledávání důkazů a (III) metody, jež samostatně vymýšlejí vhodné dokazovací strategie pro dané třídy problémů. Ukážu příklady systé…
Organizer
Pražský informatický seminář
Account · 74 followers
About Pražský informatický seminář
Seminář se bude scházet vždy 4. čtvrtek v měsíci v 16 hod. (s výjimkou letních měsíců a prosince), a to buď v budově FEL ČVUT na Karlově náměstí, nebo v budově MFF UK na Malostranském náměstí. Jeho program bude tvořen hodinovou přednáškou, po níž bude následovat časově neomezená diskuse. Základem přednášky by mělo být něco (v mezinárodním měřítku) mimořádného nebo aspoň pozoruhodného, na co přednášející přišel a co vysvětlí způsobem srozumitelným a zajímavým i pro širší informatickou obec. Přednášky budou standardně v angličtině. Formát semináře připravil přípravný výbor ve složení Roman Barták (MFF UK), Michal Chytil (ÚI AVČR), Pavel Kordík (FIT ČVUT), Jan Kybic (FEL ČVUT), Michal Pěchouček (FEL ČVUT), Jiří Sgall (MFF UK), Vojtěch Svátek (FIS VŠE), Michal Šorel (ÚTIA AV ČR), Tomáš Werner (FEL ČVUT), Filip Železný (FEL ČVUT) Idea Pražského informatického semináře vznikla z rozhovorů představitelů několika vědeckých institucí na téma, jak odstranit zbytečnou fragmentaci informatické komunity v ČR.
Like the format? Trust SlidesLive to capture your next event!
Professional recording and live streaming, delivered globally.
Sharing
Recommended Videos
Presentations on similar topic, category or speaker
Machine Translation of Natural Languages
Watch later
Total of 0 viewers voted for saving the presentation to eternal vault which is 0.0%
Talking to the brain in its own language: from simulations to cortical implants
Watch later
Total of 0 viewers voted for saving the presentation to eternal vault which is 0.0%
Symmetry in Computational Complexity
Watch later
Total of 0 viewers voted for saving the presentation to eternal vault which is 0.0%
GraalVM - the fastest virtual machine
Watch later
Total of 0 viewers voted for saving the presentation to eternal vault which is 0.0%
Sorting and Searching for Algorithmic Intelligence
Watch later
Total of 0 viewers voted for saving the presentation to eternal vault which is 0.0%
Teams of autonomous cooperating micro aerial vehicles: From theory to applications
Watch later
Total of 0 viewers voted for saving the presentation to eternal vault which is 0.0%