Семинар Катедре за рачунарство и информатику, 22. март 2018.
- 20. Март, 2018
- Коментари (0)
Наредни састанак Семинара биће одржан у четвртак, 22. марта 2018. у сали 718 Математичког факултета са почетком у 18:15 часова.
Предавач: проф. др Филип Марић
Наслов предавања: БРЗ ФОРМАЛНИ ДОКАЗ ЕРДОШ-СЕКЕРЕШОВЕ ХИПОТЕЗЕ ЗА КОНВЕКСНЕ ПОЛИГОНЕ СА НАЈВИШЕ 6 ТАЧАКА
Апстракт: Хипотеза коју су формулисали Клајн и Секереш 1932 (данас позната под именом "Ердош-Секерешова хипотеза" или "Хипотеза са срећним крајем") тврди за свако m>=3 сваки скуп који садржи 2^(m-2)+1 тачку у општем положају (никоје три различите тачке нису колинеарне) садржи конвексни m-троугао. Хипотеза је потврђена за свако m<=6. Случај m=6 су недавно решили Секереш и Петерс помоћу рачунарске претраге која је конзумирала "више од 3000 GHz часова".
Описујемо доказ који је унапређен у неколико смерова. Помоћу промене репрезентације, разматрања симетрија и помоћу модерних САТ решавача, смањили смо време доказа на око само пола сата на обичном личном рачунару (тј. наш доказ захтева само око 1 GHz час). Такође, формализовали смо доказ у доказивачу Isabelle/HOL, што га чини много поузданијим.
Коментари(0)