ОК Прил 1
Фундаментальная основа программирования –
математическая логика и теория алгоритмов
В теории алгоритмов были предугаданы основные концепции, которые легли в основу принципов построения и функционирования ВМ с программным управлением и принципов создания языков программирования
Алгоритм
 |  |
Машина Тьюринга Рекурсивные Нормальные λ-исчисление
функции алгорифмы
Тьюринг
Пост Черч Марков Скотт
Клини
Гедель
Эрбран
Четыре главные модели алгоритма породили разные направления
в программировании
Алгоритмическая логика (динамическая логика, программная логика, логика Хоара) – раздел теоретического программирования, в рамках которого исследуются алгоритмические системы, представляющие средства для задания синтаксиса и семантики языков программирования, а также для синтеза компьютерных программ и их верификации (проверки правильности работы)
Алгоритм, который проверяет отношение
H1, H2, …, Hk ├ Т F,
где H1, H2, …, Hk – гипотезы, F – некоторая формула теории Т,
называется алгоритмом автоматического доказательства теорем
Метод резолюций был разработан американским ученым Робинсоном (1965 г.)
Т. (о полноте метода резолюций) Множество дизъюнктов G = {H1, H2, …, Hk} противоречиво Û существует резолютивный вывод из G, оканчивающийся 0 (тождественно ложной формулой)
F1, F2,..., Fm ├ H Û F1, F2,..., Fm ╞ H Û F1, F2,..., Fm, 7H ╞ Û
Û F1 Ù F2 Ù... ÙFmÙ 7H ╞ Û D1 Ù D2 Ù... Ù Dk╞
ОК Прил 2
Метод резолюций в ИП
Особая стандартная форма – предложения
Преобразование формулы ИП в множество предложений осуществляется по схеме:
элиминация импликации Þ
протаскивание отрицаний Þ
разделение связанных переменных Þ
приведение к предваренной форме Þ
элиминация кванторов существования (сколемизация) Þ
элиминация кванторов общности Þ
приведение к КНФ Þ
элиминация конъюнкции
Проверьте правильность заключения методом резолюций
«Все люди смертны. Сократ – человек. Следовательно, Сократ смертен.»
Унификатор
Алгоритм унификации
В ИП метод резолюций является частичным алгоритмом автоматического доказательства теорем
Стратегии поиска (зачем они нужны?)
Нисходящая стратегия
Хорновские дизъюнкты
7X1Ú7X2Ú...Ú7Xn или 7X1Ú7X2Ú...Ú7XnÚY
Алгоритм проверки невыполнимости множества хорновских дизъюнктов S
