Математическая логика и теория алгоритмов

Литера называется позитивной, если она не содержит отрица­ ния, и негативной, если его содержит. Дизъюнкт D называется хорновским, если он содержит не более одной позитивной литеры. Примеры хорновских дизъюнк­ тов: А. В, I a, 1 В, " k v l CvB, 1 Jv~\ В, "UvlCvl CvD. В общем случае хорновский дизъюнкт можно представить в виде l4iv"k2V...v"l4 „v5 или 1^ i v ] ^2V...vl ri>\, или При этом дизъ­ юнкт 1 ^ i v ] AjV-.-v] А„\/В называют точным, дизъюнкт 1 1v l aiv.. .v]a „ — негативным, а дизъюнкт А - унитарным позитив­ ным дизъюнктом. Рассмотрим множество S хорновских дизъюнктов без тавтоло­ гий. Невыполнимость можно проверить с помощью следующего алгоритма. 1. Полагаем; что 6^= S. 2. Пусть S"'^, п>\, построено. Для построения S" выбираем из 5'дизъюнкты D\ и Di такие, что: D\ - унитарный позитивный дизъюнкт, пусть, например, D\=P; Di - дизъюнкт, содержащий литеру I Р. Вычисляем резольвенту R для дизъюнктов Z)i и А и полагаем, что S" - Z)2})'^{^}. Эту процедуру повторяем до тех пор, пока не получим пустой дизъюнкт • либо пока не ока>кется, что в iS* не существует дизъюнктов D\ и D2 указанных видов. Можно доказать, что для приведенного алгоритма появление пустого дизъюнкта означает, что мноисество S хорновских дизъюнктов невыполнимо. Если же окалсется, что 5""' не содержит дизъюнктов Di и Dj указанных видов, то исходное множество 5" хорновских дизъ­ юнктов выполнимо. Реализацию этого алгоритма прюще проводить с помощью таблицы. Продемонстрируем это на примере. Пусть имеем множество хорновских дизъюнктов: 5'={Pv1 Q v l R, Т, Q, Pv ] Qy \ U, T, 1P v ] g v ] T). Выпиваем дизъюнкты из 5° = 5 в ячейки нулевой строки приводимой далее таблицы. Каждая п-я строка содержит дизъюнкты из S п > 0. 101