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

ОК Прил 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

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

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

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

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

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

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

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

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

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