Алексей Терехов, Надежда Коржавина, Дмитрий Грибанов, "Автоматическое доказательство теорем"  

Аннотация 

Введение в математическую логику, как способ формализации человеческой логики: 

• Логика высказываний 
• Логика первого порядка 
• Математическая теория (аксиоматическое и структурное задание) 
• Математика парадоксальна и может быть противоречива — Теоремы Гёделя, проблемы вытекающие из теорем Геделя 

Введение в автоматическое доказательство теорем: 

• Стандартная форма записи 
• Теорема Эрбрана
• Один из первых алгоритмов авт. док. - метод Гилмора, его модификация (Девис, Патнем). 
• Метод резолюции — 1-ый эффективный метод авт. док-ва. 
• Стратегии вычеркивания, поддержки. 
• Некоторые известные виды резолюции: семантическая, линейная, лок резолюции; и некоторые их модификации и уточнения.
• Какой метод применяется в ПРОЛОГЕ?; Дизъюнкты Хорна. 
• Невыполнимость в специальных классах моделей, пример на основе резолюции с равенствами, парамодуляция. 
• Приминение: анализа, синтез программ, решение задач, дедуктивный вывод, обучаемость. 

Введение в логическое программирование (на основе языка ПРОЛОГ) 

• Как выглядит программа на прологе? 
• Основы написания логических программ. 
• Примеры программ. 

Специальных знаний не требуется, т. к. включено введение в мат. логику. 

Лекция для тех, кто желает расширить свой кругозор.

<< вернуться  |   Документ от: 23.04.2009 10:45