Приложения математической логики (Прил)

ОК Прил 1

 

Фундаментальная основа программирования –

математическая логика и теория алгоритмов

 

В теории алгоритмов были предугаданы основные концепции, которые легли в основу принципов построения и функционирования ВМ с программным управлением и принципов создания языков программирования

Алгоритм

 

Машина Тьюринга Рекурсивные Нормальные λ-исчисление

функции алгорифмы

Тьюринг

Пост Черч Марков Скотт

Клини

Гедель

Эрбран

Четыре главные модели алгоритма породили разные направления

в программировании

 

Алгоритмическая логика (динамическая логика, программная логика, логика Хоара) – раздел теоретического программирования, в рамках которого исследуются алгоритмические системы, представляющие средства для задания синтаксиса и семантики языков программирования, а также для синтеза компьютерных программ и их верификации (проверки правильности работы)

 

Алгоритм, который проверяет отношение

H₁, H₂, …, H_k ├ _Т F,

где H₁, H₂, …, H_k – гипотезы, F – некоторая формула теории Т,

называется алгоритмом автоматического доказательства теорем

 

Метод резолюций был разработан американским ученым Робинсоном (1965 г.)

Т. (о полноте метода резолюций) Множество дизъюнктов G = {H₁, H₂, …, H_k} противоречиво Û существует резолютивный вывод из G, оканчивающийся 0 (тождественно ложной формулой)

 

F₁, F₂,..., F_m ├ H Û F₁, F₂,..., F_m ╞ H Û F₁, F₂,..., F_m, 7H ╞ Û

Û F₁ Ù F₂ Ù... ÙF_mÙ 7H ╞ Û D₁ Ù D₂ Ù... Ù D_k╞

 

ОК Прил 2

 

Метод резолюций в ИП

 

Особая стандартная форма – предложения

 

Преобразование формулы ИП в множество предложений осуществляется по схеме:

элиминация импликации Þ

 

протаскивание отрицаний Þ

 

разделение связанных переменных Þ

 

приведение к предваренной форме Þ

 

элиминация кванторов существования (сколемизация) Þ

 

элиминация кванторов общности Þ

 

приведение к КНФ Þ

 

элиминация конъюнкции

 

Проверьте правильность заключения методом резолюций

«Все люди смертны. Сократ – человек. Следовательно, Сократ смертен.»

 

Унификатор

Алгоритм унификации

 

В ИП метод резолюций является частичным алгоритмом автоматического доказательства теорем

Стратегии поиска (зачем они нужны?)

 

Нисходящая стратегия

Хорновские дизъюнкты

7X₁Ú7X₂Ú...Ú7X_n или 7X₁Ú7X₂Ú...Ú7X_nÚY

 

Алгоритм проверки невыполнимости множества хорновских дизъюнктов S