Метод семантической резолюции

Как отмечалось, в процессе поиска вывода пустого дизъюнкта методом резолюции генерируется некоторая совокупность излишних, ненужных для вывода, дизъюнктов. Одним из способов уменьшения числа генерируемых излишних дизъюнктов является введение интерпретации.

Интерпретацией для набора входящих в дизъюнкт букв (переменных) X ₁, X ₂, …, X_n является n - мерный булев вектор Е (е ₁, е ₂,..., е_n); переменной X_i присваивается логическое значение "истина" ("ложь"), если е_i = 1 (соответственно е_i = 0). При интерпретации Е дизъюнкты исходной совокупности M и порождаемые резольвенты разбиваются на два подмножества – S ₁, содержащее дизъюнкты, при данной интерпретации обращающиеся в истину, и S ₂, включающее дизъюнкты, обращающиеся в ложь.

Метод семантической резолюции предусматривает, что при образовании каждой следующей резольвенты используется один дизъюнкт множества S ₁и один дизъюнкт множества S ₂.

Пример 7. Рассмотрим совокупность дизъюнктов из примера 5:

1) A А'; 2) В В'; 3) A B; 4) A В';

5) В А'; 6) А' В'; 7) В' А'.

Примем следующую интерпретацию: A = 1; A^' = 0; В =1; В' = 0. Укажем номера формул, входящих в множество S ₁: 3, 4, 5, 6, 7; номера формул, входящих в множество S ₂, следующие: 1, 2. Применим метод семантической резолюции (перед каждым дизъюнктом указываем его порядковый номер, после дизъюнкта в скобках вписываем номера порождающих дизъюнктов и множества, S ₁ или S ₂, которому принадлежит полученный дизъюнкт):

8) А' В (1,3; S ₁);

9) А' В (2,6; S ₂);

10) А' (8,9; S ₂);

11) В' (7,10; S ₂);

12) A (4,11; S ₂);

13) В (3,12; S ₁);

14) В (5,10; S ₂);

15) ÿ (13,14).

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

Доказательство может быть выполнено для любой фиксированной интерпретации,

Верхняя оценка временной вычислительной сложности метода семантической резолюции экспоненциальна.

Дата добавления: 2015-06-27