|
Экран компьютера с работающей на нем автоматической программой для доказательств Agna 2. Фото пользователя Norfolk с сайта wikipedia.org
|
В рамках четвертой международной конференции по автоматизированной формулировке логических выводов (The 4th International Joint Conference on Automated Reasoning) в Сиднее, Австралия, состоятся соревнования компьютерных программ, предназначенных для решения логических задач и доказательства теорем (такие программы называются дедуктивными). Победитель получит приз в три тысячи долларов США. Об этом сообщается на официальном сайте конференции.
Для решения участникам будут предложены задачи различной степени сложности: от простых логических игр и математических примеров до построения алгоритма действий в случае террористической атаки на крупный населенный пункт.
Это уже 22-е по счету подобные соревнования. В этом году в них принимает участие более 20 программных продуктов, разработанных как отдельными энтузиастами, так и целыми лабораториями. Большинство программ находятся в свободном доступе в интернете.
Автоматизированная дедукция является одной из самых развитых областей автоматизированной формулировки логических выводов раздела науки, которой занимается применением компьютеров для решения различных логических задач. У дедуктивных программ есть ряд теоретических недостатков. Если утверждение верно, то программа рано или поздно способна его доказать. Если же утверждение неверно, то она не в состоянии указать на это. Обычно эти программные продукты устроены таким образом, что после определенного времени они просто выдают сообщение о том, что либо задача слишком сложна, либо не имеет решения.
