Метод резолюций в логике высказываний
Метод резолюций применяется для доказательства того, что формула G является логическим следствием формул . При этом доказывается невыполнимость множества формул .
Опр. (повторно). Литерал атомарная формула (кроме 0 и 1), или ее отрицание.
Дизъюнкт (элементарная дизъюнкция) литерал или дизъюнкция литералов.
Опр. Пустой дизъюнкт дизъюнкт, не содержащий литералов.
Пустой дизъюнкт ложен при любой интерпретации.
Опр. Противоположные литералы литералы X и X.
Опр. Правилом резолюций в логике высказываний называется:
из дизъюнктов (X F1) и (X F2) выводится дизъюнкт (F1 F2).
Опр.
Пусть S
множество дизъюнктов. Будем говорить,
что дизъюнкт
выводится из S,
если существует последовательность
дизъюнктов
,
такая, что каждый
принадлежит S
или получен
по правилу резолюций из дизъюнктов
.
Вывод из S эта последовательность .
Теорема.
Множество дизъюнктов S невыполнимо из S выводится пустой дизъюнкт.
Схема применения метода резолюций.
Дано:
.
1.
Формулы
приводятся к КНФ.
2. Все получившиеся дизъюнкты собирают в множество S.
3. Строится вывод □ из S.
Предикаты и операции с ними. Формулы.
Опр. Пусть M . Назовём n-местным предикатом, заданным на M выражение, содержащее n переменных, обращающееся в высказывание при замене переменных элементами из M.
Обозначение:
.
Опр. Назовём нульместным предикатом высказывание.
Операции с высказываниями переносятся на предикаты:
конъюнкция, дизъюнкция, отрицание, импликация, эквиваленция.
Например, для конъюнкции новое определение формулируется так:
Опр.
Пусть
и
n-местные
предикаты, заданные на M.
Конъюнкцией этих предикатов называется
новый предикат
,
такой, что для любых элементов
высказывание
.
Кроме этих пяти операций введём ещё две операции навешивания кванторов.
Опр.
Пусть
n-местный
предикат, заданный на M,
y переменная
(либо совпадающая с
,
либо новая). Назовём предикатом,
полученным навешиванием квантора
общности на
выражение «Для любого y выполняется
».
Обозначение:
.
Опр. Пусть n-местный предикат, заданный на M, y переменная (либо совпадающая с , либо новая). Назовём предикатом, полученным навешиванием квантора существования на выражение «Существует y, такой, что выполняется ».
Обозначение:
.
Опр. Термом называется выражение одного из двух видов:
1) переменная или константа (символ нуль-местной функции);
2)
,
где
,
термы.
Опр. Атомарной формулой называется выражение
,
где
,
термы.
Опр. Формулой логики предикатов называется выражение одного из двух видов:
1) Атомарная формула;
2) (F) & (G), (F) (G), (F), (F) (G), (F) (G), (y)(F), (y)(F),
где F и G формулы логики предикатов, y переменная.
Опр. В формулах (y)(F), (y)(F), формула F называется областью действия квантора по переменной y.
Для уменьшения количества скобок договоримся о приоритетах операций: у кванторов выше, чем у связок, для связок также, как в высказывания.