Пример с трассировочной таблицей

↑

▷ Содержание

⇐ ПредыдущаяСтр 2 из 6Следующая ⇒

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

1) под литералом будем понимать атомарную формулу или ее отрицание;

2) под дизъюнктом будем понимать литерал, а также дизъюнкцию литералов;

3) -пустой дизъюнкт, не содержит литералов (ложная атомарная формула);

4) формула F V равносильна F

5)формула F &равносильна 

6)Литералы L и L называются противоположными

Методом резолюций называется последовательное получение бинарных резольвент из данных дизъюнктов и вновь получаемых дизъюнктов.

Резольвента.

Пусть для дизъюнктов  и  существует литера  в , которая контрарна литере  в . Вычеркнув и  из  и  соответственно, построим дизъюнкцию оставшихся частей  и Полученный таким образом дизъюнкт называется (бинарной) резольвентой  и , его часто обозначают через R.

Пусть ,  , тогда ,

Нахождение резольвенты.

Алгоритм логического вывода с использованием метода резолюций:

1)занести в массив А исходные дизъюнкты из множества S

2)найти первую пару дизъюнктов, имеющих контрарную пару и их резольвенту

3)если пара дизъюнктов не найдена, тогда:

3.1 прервать вывод

4)пока нет вывода пустого дизъюнкта и нет прерывания вывода:

4.1 занести резольвенту (новый дизъюнкт) в массив А

4.2 найти следующую пару дизъюнктов, имеющих контрарную пару и их резольвенту

4.3 если пара дизъюнктов не найдена:

4.3.2 прервать вывод

5) если произошло прерывание вывода, тогда:

5.1 сформулировать сообщение о неуспешном выводе

6) если не произошло прерывание логического вывода, тогда

6.1 сформулировать сообщение об успешном выводе

Доказательство теоремы.

Теорема. Множество дизъюнктов логики высказываний S невыполнимо тогда и только тогда, когда из S выводим пустой дизъюнкт.

Пусть S = { }

Последовательность

1.  (из S)

2.  (из S) 

3. (резольвента: X V Y V Z и  Y V U

4.  (из S) 

5. (резольвента: X V Z V U и ) – вывод из S

Дизъюнкт Z V U выводим из S

10. Проблема согласования контрарных пар. Подстановка. Переменная активная для подстановки. Элементарная подстановка. Применение подстановки к логическому выражению. Унификатор.

Познавательные статьи:



Техника прыжка в длину с разбега

Тактические действия в защите

История Олимпийских игр

История развития права интеллектуальной собственности