15. Метод резолюций в логике высказываний. Корректность и полнота метода резолюций.

Метод резолюцийнаиболее эффективный способ алгоритмического доказательства

Доказательство в методе резолюций

строится путем опровержения.

Введем некоторые дополнительные понятия.

2. Литерал – это произвольный атом или его отрицание.

3. Дизъюнктэто дизъюнкция конечного множества литералов.

Множество дизъюнктов соответствует представленному в КНФ высказыванию

Пусть D1 и D2 дизъюнкты, L – атом. Резольвентой двух дизъюнктов (D1L) и (D2L) называется дизъюнкт (D1D2).

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

Доказательство методом резолюции является аналогом доказательства от противного. В утверждении о следовании из множества посылок некоторого заключения производят замену этого заключения его отрицанием. Затем каждую посылку и отрицание заключения представляют в виде множества дизъюнктов и применяют к полученному множеству дизъюнктов метод резолюции.

Множество дизъюнктов S невыполнимо тогда и только тогда, когда существует резолютивный вывод пустого дизъюнкта из S.

Полнота метода резолюций состоит в том, что он гарантирует получение для формулы пустой резольвенты, если множество дизъюнктов S невыполнимо. Если же пустая резольвента не найдена, то множество S не является невыполнимым.

16. Термы и формулы в логике предикатов. Интерпретация термов и формул.

Термы являются аргументами предикатных символов. Понятие терма сигнатуры  определяется индуктивно:

• всякая предметная переменная хV и всякая константа сС являются термом;

• если t₁,t ₂,...,t _{n -} термы, а fF, f- функциональный символ местности n сигнатуры , то выражение вида f (t_1,t ₂,...,t _nn) является термом.

• других термов нет.

Индуктивное определение формулы:

• предикатный символ r (t₁,t ₂,...,t_r )R, где t₁,t ₂,...,t _n -термы сигнатуры , есть атомная формула или атом;

• если А и В  формулы, то АВ, А&В, АВ, АВ, А – формулы; в общем случае формула может быть образована любыми логическими связками, определенными в логике высказываний;

• если А(х) – формула, то выражения хА(х) и хА(х) - формулы. Здесь х , х называются кванторными приставками, х  переменная кванторной приставки, А(х) - область действия кванторной приставки; в этих случаях говорят, что переменная х входит в формулу связанно, или что имеет место связанное вхождение переменной х;

• других формул нет.

Формула А называется постоянной или предложением, если она не содержит свободных вхождений переменных. В противном случае формула называется параметрической или условием.

Одна и та же переменная может входить в формулу как связанно, так и свободно. Например,

1. А(х₁,х₂) — переменные х₁ и х₂ входят свободно;

2. А(х₁,х₂)х₁ В(х₁) — первое вхождение переменной х₁ свободно, второе - связано. Переменная х₂ входит свободно.

3. х₂ (В (х₁,х₂)х₁А(х₁)) — первое вхождение переменной х₁ свободно, второе – связано, переменная x₂ входит в формулу

Сами по себе термы  ничего не выражают, пока не определена семантика языка, т.е. интерпретация символов. Интерпретация I[t] ставит в соответствие каждому символу константы сигнатуры  конкретный объект из предметной области, т.е. функция интерпретации константы I_C:CD. Предметные переменные, от которых терм зависит, пробегают предметную область, т.е. последовательно принимают все возможные значения в D.Для термов, определенных по второму пункту правила, функция интерпретации терма f(t₁,t₂,…,t_n), где i (t_i – терм), а f – n-местный функциональный символ, определяется следующим образом: I[f(t₁,t₂,…,t_n)] = I[f](I[t₁],I[t₂],…,I[t_n]). Интерпретация I_F означает отображение функционального символа в предметную область, которое ставит в соответствие каждой упорядоченной n-ке значений аргументов функционального символа fⁿF конкретный объект из D, равный значению этого функционального символа, т.е. I_F: DⁿD. можно говорить только об интерпретации постоянных термов.

Интерпретацией формулы в данной модели называется отображение I_R:Dⁿ{0,1}, которое ставит в соответствие каждой упорядоченной n-ке аргументов предикатного символа логическое значение 0 (ложь) или 1 (истина). В выбранной интерпретации всякой замкнутой формуле ставится в соответствие ее логическое значение, а всякой формуле, содержащей свободные вхождения переменных – ее таблица, соответствующая всем возможным интерпретациям параметрических термов, являющихся ее аргументами. Логическое значение формулы I[A]. Для постоянной формулы 0 или 1, для формулы, содержащей свободные вхождения переменных - вектор, элементами которого являются 0 и 1, длина которого зависит от числа различных наборов значений свободных переменных в данной предметной области.

Для параметрических формул функция интерпретации определяет значение формулы на каждом из возможных наборов значений переменных в предметной области.

число различных интерпретаций предикатного символа равно 2^р. Соответственно, интерпретация задается парой (D, I_s), где I_s — выбранная функция интерпретации Логическое значение формул, содержащих кванторную приставку по переменной х, определяется для квантора существования  как максимум из логических значений формулы, когда переменная кванторной приставки «пробегает» всю предметную область, и как минимум для квантора общности 