2. Базис логического программирования

Интерпретировать формулу логики высказываний, значит приписать значения истинности составляющим ее элементарным высказываниям и вычислить истинностное значение всей формулы.

Элементарное высказывание (буква) является формулой нулевого уровня. Если элементарное высказывание всегда верно, мы будем его обозначать буквой И, а если оно всегда неверно, — буквой Л. Тогда формулы первого уровня — это элементарные высказывания, к которым применена только одна логическая связка.

Пусть Ф1 и Ф2 — формулы ненулевого уровня. Тогда записи (¬(Ф1)), ((Ф1)&(Ф2)), ((Ф1)V(Ф2)), ((Ф1)->(Ф2)), ((Ф1)~(Ф2)) также являются формулами. Если же одна из формул Ф1 и Ф2 , к которым применяется логическая связка, имеет нулевой уровень, то она в скобки не заключается.

Формула — это либо атом, либо одна из следующих конструкций: , где F,F₁,F₂ — формулы, а x — переменная.

Переменная x называется связанной в формуле F, если F имеет вид либо , или же представима в одной из форм , причем x уже связанна в H, F₁ и F₂. Если x не связанна в F, ее называют свободной в F. Формулу без свободных переменных называют замкнутой формулой, или предложением. Теорией первого порядка называют любое множество предложений.

Логика первого порядка обладает рядом полезных свойств, которые делают ее очень привлекательной в качестве основного инструмента формализации математики. Главными из них являются полнота (это означает, что для любой формулы выводима либо она сама, либо ее отрицание) и непротиворечивость (ни одна формула не может быть выведена одновременно со своим отрицанием). При этом если непротиворечивость более или менее очевидна, то полнота — нетривиальный результат полученный Гёделем в 1930 году (теорема Гёделя о полноте). По сути теорема Гёделя устанавливает фундаментальную эквивалентность понятий доказуемости и общезначимости.

Система логических аксиом логики первого порядка состоит из аксиом исчисления высказываний дополненной двумя новыми аксиомами:

,

,

где A[t / x] — формула, полученная в результате подстановки терма t вместо переменной x в формуле A.

Правил вывода 2:

Modus ponens:

Правило обобщения (GEN):

Под упрощением формулы, не содержащей операций импликации и эквиваленции, понимают равносильное преобразование, приводящее к формуле, которая либо содержит по сравнению с исходной меньшее число операций конъюнкции и дизъюнкции и не содержит отрицаний неэлементарных формул, либо содержит меньшее число вхождений переменных.

Коммутативность: x y = y x, {&, }.

Идемпотентность: x x = x, {&, }.

Ассоциативность: (x y) z = x (y z), {&, }.

Дистрибутивность конъюнкций и дизъюнкции относительно дизъюнкции, конъюнкции и суммы по модулю два соответственно:

x (y z) = (x y) (x z),

x (y z) = (x y) (x z),

x (y z) = (x y) (x z).

Законы де Мо́ргана:

(x y) = ( x) ( y),

(x y) = ( x) ( y).

Законы поглощения:

x (x y) = x,

x (x y) = x.

Другие (1):

x ( x) = x 0 = x x = 0.

x ( x) = x 1 = x x = x x = 1.

x x = x x = x 1 = x 0 = x 0 = x.

x 1 = x 0 = x 0 = x x = x x = x.

.

Другие (2):

= = .

= = = = .

= = .

Другие (3) (Дополнение законов де Мо́ргана):

= = .

= = .

Следующая формальная грамматика описывает все формулы, приведенные к КНФ:

<КНФ> → <дизъюнкт>

<КНФ> → <КНФ> ∧ <дизъюнкт>

<дизъюнкт> → <литерал>

<дизъюнкт> → (<дизъюнкт> ∨ <литерал>)

<литерал> → <терм>

<литерал> → ¬<терм>

где <терм> обозначает произвольную булеву переменную.

Исчисление высказываний

Пусть C₁ и C₂ - два предложения в исчислении высказываний, и пусть , а , где P - пропозициональная переменная, а C'₁ и C'₂ - любые предложения (в частности, может быть, пустые или состоящие только из одного литерала).

Правило вывода

называется правилом резолюции.

Предложения C₁ и C₂ называются резольвируемыми (или родительскими), предложение - резольвентой, а формулы P и - контрарными литералами.

Исчисление предикатов

Пусть C₁ и C₂ - два предложения в исчислении предикатов.

Правило вывода

называется правилом резолюции в исчислении предикатов, если в предложениях C₁ и C₂ существуют унифицированные контрарные литералы P₁ и P₂, то есть , а , причём атомарные формулы P₁ и P₂ являются унифицируемыми наиболее общим унификатором σ.

В этом случае резольвентой предложений C₁ и C₂ является предложение , полученное из предложения применением унификатора σ. ^[2]

Пример: вывод решения в логической модели на основе метода резолюций.

Даны утверждения:

• «Сократ – человек»;

• «Человек – это живое существо»;

• «Все живые существа смертны».

Требуется методом резолюций доказать утверждение «Сократ смертен».

Решение:

Шаг 1. Преобразуем высказывания в дизъюнктивную форму:

Шаг 2. Запишем отрицание целевого выражения (требуемого вывода), т.е. «Сократ бессмертен»:

Шаг 3. Cоставим конъюнкцию всех дизъюнктов (т. е. построим КНФ), включив в нее отрицание целевого выражения:

Шаг 4. В цикле проведем операцию поиска резольвент над каждой парой дизъюнктов:

Получение пустого дизъюнкта означает, что высказывание «Сократ бессмертен» ложно, значит истинно высказывание «Сократ смертен».