Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

(5) 20. Аналогично получим: (6)26 v s - . 6 из(1)и(4), (J)6QV4^Q ИЗ(2)И(3), (8)4-. Q ИЗ (2) И (4), (9) => из (5) и (8). Можно доказать следующую теорему для лок-резолюции Теорема 3.7. Пусть S - множество дизъюнктов, в котором каждая литера индексирована целым числом. Если S противоречиво (невыполнимо), то имеется лок-вывод пустого дизъюнкта =жз S. § 6. Метод резолюций для хорновских дизъюнктов Литера называется позитивной, если она не содержит отрицания, и негативной, если содержит отрицание. Дизъюнкт D называется хорновским, если он содержит не более одной позитивной литеры. Примеры хорновских дизъюнктов: А, В, —Л, —S, —Av — iC vB, —Л V —iB. В общем случае хорновский дизъюнкт можно представить в виде— u 4 2 V . . . v —AnVB или —AiV—A2V... v—An,n>l, или A. Дизъюнкт, содержащий только одну позитивную литеру, называется унитарным позитивным дизъюнктом. Рассмотрим множество S хорновских дизъюнктов без тавтологий. Невыполнимость S можно проверить с помощью следующего алгоритма. 1. Полагаем, что S. 2. Пусть S п>1, построено. Для построения S " выбираем из S дизъюнкты Di и D2 такие, что: Di - унитарный позитивный дизъюнкт, пусть, например, Di=P; D2- дизъюнкт, содержащий литеру —iP. Вычисляем резольвенту R для дизъюнктов D7 и и полагаем, что = (S D 2})u{ R }. Эту процедуру повторяем до тех пор, пока получим пустой дизъюнкт либо окажется, что в S не существует дизъюнктов Di ^ D2 указанных видов. Можно доказать, что для приведенного алгоритма появление пустого дизъюнкта означает, что множество S хорновских дизъюнктов невыполнимо. Если же окажется, что S не содержит дизъюнктов Di ^ D2 указанных видов, то исходное множество S хорновских дизъюнктов выполнимо. Реализацию этого алгоритма проще проводить с помощью таблицы. Продемонстрируем это на примере. Пусть имеем множество хорновских дизъюнктов: 68