Меню
Главная
Авторизация/Регистрация
 
Главная arrow Математика, химия, физика arrow ДИСКРЕТНЫЙ АНАЛИЗ. ФОРМАЛЬНЫЕ СИСТЕМЫ И АЛГОРИТМЫ
Посмотреть оригинал

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

В силу корректности ИВ построение вывода даёт доказательство тавтологичности формулы. Однако вывод, который строится в соответствии с первым доказательством теоремы полноты, требует фактически перебора всех возможных значений переменных. Это ничем не лучше прямого использования определения тавтологии.

В этом разделе мы обсудим другой способ доказательства тавтологичности формулы — метод резолюций. Этот

способ во многих случаях позволяет доказывать тавтоло- гичность быстрее, поэтому он (и его модификации для более сложных формальных систем) широко применяется в компьютерных системах построения доказательств.

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

КНФ

Метод резолюций работает с формулами в конъюнктивной нормальной форме (КНФ). Напомним, что это такое. Литерал — это переменная или отрицание переменной. Дизъюнкт — это формула, которая является дизъюнкцией литералов. Пустой дизъюнкт по определению означает ложь. Конъюнктивная нормальная (форма (КНФ) — это формула, которая является конъюнкцией дизъюнктов.

Заметим, что переход к КНФ не ограничивает общности метода.

В самом деле, по любой формуле А с переменными х...., хп можно построить равносильную ей КНФ. Для этого по каждому набору значений переменных а = (ал,..., ап), на котором А ложна, построим дизъюнкт

где, как обычно, х1 = х, х° = ~х. Так как Xх = 1, а хЛх = О, дизъюнкт D(a) обращается в 0 в точности на наборе а. Поэтому конъюнкция D(a) по всем наборам значений переменных, на которых формула А ложна, равносильна А:

Формула (1.14) отвечает на вопрос о равносильности произвольных формул и КНФ. Но КНФ из формулы (1.14) в общем случае очень длинная: нулей у булевой функции от п переменных может быть 2”. Если нас интересует лишь выполнимость формулы А, то довольно просто написать более короткую КНФ, выполнимость которой равносильна выполнимости формулы А. Для каждой подформулы В формулы А (см. определение на с. 21) введём переменную zb- Если подформула В имеет вид 1D, то построим по (1.14) КНФ, равносильную формуле 2д ~ Izp. Если подформула В имеет вид D-tE, то построим по (1.14) КНФ, равносильную формуле zb ~ (гр—>ze)- Конъюнкция этих КНФ и дизъюнкта za образует КНФ С(А), выполнимость которой равносильна выполнимости формулы А. По индукции легко проверить, что истинность КНФ С{А) на наборе значений zx = ах, где X пробегает все подформулы А, в том числе и переменные, входящие в формулу А, равносильна тому, что значение любой подформулы В на наборе значений переменных х, = <хх> равно zb, причём значение za равно 1 (т. е. формула А выполнима на наборе ж, = aXi).

Количество дизъюнктов в КНФ С (А) легко оценить через количество связок т формулы А. Каждой связке в формуле А соответствует КНФ, равносильная формуле из не более чем 3 переменных. У булевой функции от 3 переменных не более 8 нулей. Значит, общее количество дизъюнктов в С (А) не превосходит 1 + 8те.

 
Посмотреть оригинал
< Предыдущая   СОДЕРЖАНИЕ   Следующая >
 

Популярные страницы