Представление и обработка знаний

70 8) пусть S – множество дизъюнктов. Выводом из S называет- ся последовательность дизъюнктов: D 1 , D 2 , ..., D n такая, что каждый дизъюнкт этой последовательности принадлежит S или следует из предыдущих по правилу резолюций; 9) дизъюнкт D выводим из S , если существует вывод из S , по- следним дизъюнктом которого является D . Например, если S = {  X  Y  Z ,  Y  U , X }, то последова- тельность: D 1 =  X  Y  Z (взят из S ), D 2 =  Y  U (взят из S ), D 3 =  X  Z  U (резольвента:  X  Y  Z и  Y  U ) , D 4 = X (взят из S ), D 5 = Z  U (резольвента:  X  Z  U и X ) является выводом из S , а дизъюнкт Z  U выводим из S . Приведем без доказательства следующую теорему: «Множе- ство дизъюнктов логики высказываний S невыполнимо тогда и только тогда, когда из S выводим пустой дизъюнкт». Пусть дана модель: M = D 1 & D 2 & … & Dr , D 1, D 2, …, Dr , – дизъюнкты . Логическое выражение M принимает значение истина в за- данной интерпретации. Доказать утверждение: P . Для этого необ- ходимо доказать существование противоречия в заданной интер- претации: M &  P – ложно, т.е. невыполнима. Описание алгоритма доказательства при использовании ме- тода резолюций приведено в табл. 3.11. Рассмотрим пример доказательства методом резолюций. Пусть даны следующие правила [11]: 1. Если выигрывает команда A , то в городе A 1 праздник. 2. Если выигрывает команда B , то в городе B 1 праздник. 3. Выигрывает команда A или B. 4. Если праздник в городе A 1, то нет праздника в городе B 1. 5. Если праздник в городе B 1, то нет праздника в городе A 1.