Семинар за рачунарство и примењену математику, 23. мај 2023.

• 22. Мај, 2023
• Коментари (0)

Наредни састанак Семинара биће одржан у уторак, 23. маја у сали 301ф Математичког института САНУ са почетком у 14.15. Састанак је могуће пратити и на даљину.

Предавач: Предраг Јаничић, Математички факултет, Универзитет у Београду
 
Наслов предавања: АУТОМАТСКО ДОКАЗИВАЊЕ ТЕОРЕМА КАО РЕШАВАЊЕ ПРОБЛЕМА ОГРАНИЧЕЊА
 
Апстракт: У излагању ће бити представљен један нов приступ аутоматском доказивању теорема. За разлику од других приступа аутоматском доказивању теорема, у којима простор претраге чине формуле и оно за чиме се трага поново је формула, у овом приступу трага се за доказом као целином. Наиме, конкретан доказ у фиксираном логичком оквиру може се кодирати низом природних бројева, а синтаксичка ограничења која везују кораке доказа могу се превести у линеарна ограничења над тим бројевима. За задати скуп аксиома, задату формулу коју треба доказати и задату дужину траженог доказа, на тај начин може се добити инстанца проблема задовољивости линеарних ограничења коју аутоматски може решити одговарајући решавач. Из тог решења онда се може реконструисати тражени доказ.
 
Овај приступ има неколико својстава која немају други приступи. На пример, његовим коришћењем може се добити најкраћи могући доказ, једноставно се могу добити абдукти, једноставно се могу задати фрагменти доказа који треба допунити и једноставно се могу добити машински провериви докази.

Описани приступ примењен је на кохерентну логику (која је изражајна као логика првог реда) и имплементиран у оквиру јавно доступног доказивача Ларус. Доказивач Ларус ефикаснији је од више других доказивача за логику првог реда који генеришу машински провериве доказе.

Коаутор овог рада је проф. Julien Narboux из Француске.
 
Напомене: Напомена: Регистрациона форма за учешће на Семинару је доступна на линку:
https://miteam.mi.sanu.ac.rs/call/wnz6oyxsQsy29LfJA/MjQ__eH607WeAL9X7IFtUI98xdQQgVkp-ljiEKPPfXr

Уколико желите само да пратите предавање без могућности активног учешћа, пренос је доступан на линку:
https://miteam.mi.sanu.ac.rs/asset/YoqHWKALRkRTbK9So