Архитектура Аудит Военная наука Иностранные языки Медицина Металлургия Метрология
Образование Политология Производство Психология Стандартизация Технологии


Автоматическое доказательство теорем. Метод резолюций.



Пусть имеется множество формул Г = {A1, A2, …, An} и формула B. Автоматическим доказательством теоремы B называют алгоритм, который проверяет вывод

A1, A2, …, AnB. (3. 1)

Выражение (3.1) можно прочитать следующим образом:

Если посылки A1, A2, …, An истинны, то истинно заключение B.

или

Если причины A1, A2, …, An имели место, то будет иметь место следствие B.

Проблема доказательства в логике состоит в том, чтобы установить, что если истинны формулы A1, A2, …, An, то истинна формула B.

В общем случае такой алгоритм построить нельзя. Но для некоторых частных случаев такие алгоритмы существуют. Доказательство теоремы равносильно доказательству общезначимости некоторой формулы. Наиболее эффективно доказательство общезначимости формул осуществляется методом резолюций. Процедура поиска доказательства методом резолюций фактически является процедурой поиска опровержения, т. е. вместо доказательства общезначимости формулы доказывается, что отрицание формулы противоречиво:

A º И Û Ø A º Л.

Введем терминологию, обычно употребляемую при изложении метода резолюций.

Литерой будем называть выражения A или Ø A. Литеры A и Ø A называются контрарными, а множество {A, Ø A} – контрарной парой.

Дизъюнкт – это дизъюнкция литер (или элементарная дизъюнкция).

Пример 3.6.

A V B V C – дизъюнкт;

A V Ø B – дизъюнкт;

A V B & C – не дизъюнкт;

Ø A – дизъюнкт.

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

Рассмотрим применение метода резолюций к исчислению высказываний.

Правилом резолюции называют следующее правило вывода:

. (3. 2)

Правило (3.2) можно также записать в следующем виде:

AVB, Ø AVCB V C. (3. 3)

Правило резолюций можно доказать, используя равносильности логики высказываний:

(AVB) & (Ø AVC) É (B V C) = Ø ((AVB) & (Ø AVC)) V (B V C) = Ø (AVB) V Ø (Ø AVC) V (B V C) = Ø A& Ø B V A& Ø C V (B V C) = (Ø AV A) & (Ø AV Ø C) & (Ø BV A) & (Ø BV Ø C) V (B V C) = (Ø AV Ø C) & (Ø BV A) & (Ø BV Ø C) V (B V C) =(Ø AV Ø C V B V C) & (Ø BV A V B V C) & (Ø BV Ø C V B V C) = И.

Итак, при истинных посылках истинно заключение.

Правило (3.2) – единственное правило, применяемое в методе резолюций, что позволяет не запоминать многочисленных аксиом и правил вывода.

Дизъюнкт BVC называется резольвентой дизъюнктов AVB и Ø AVC по литере A:

BVC = resA(AVB и Ø AVC).

Если дизъюнкты не содержат контрарных литер, то резольвенты у них не существует.

Для дизъюнктов A и Ø A резольвента есть пустой дизъюнкт: resA(A, Ø A) = .

Пример 3.7.

Пусть F = A V B V C, G = Ø A V Ø B V D.

Тогда

resA(F, G) = B V C V Ø B V D.

resB(F, G) = A V C V Ø A V D.

resC(F, G) не существует.

Метод резолюций соответствует методу доказательства от противного. Действительно, условие A1, A2, …, AnB равносильно условию A1, A2, …, An, Ø B„ . Метод резолюций относится к методам непрямого вывода.

Изложим процедуру вывода A1, A2, …, AnB в виде алгоритма.

Алгоритм построения вывода методом резолюций.

Шаг 1. Формулы A1, A2, …, An и формулу Ø B привести к КНФ.

Шаг 2. Составить множество S дизъюнктов формул A1, A2, …, An и B.

Шаг 3. Вместо пары дизъюнктов, содержащих контрарные литеры записать их резольвенту по правилу (3.2).

Шаг 4. Процесс продолжаем. Если он заканчивается пустым дизъюнктом, то вывод обоснован.

Изложенный алгоритм назывется резолютивным выводом из S.

Возможны три случая:

1. Среди множества дизъюнктов нет содержащих контрарные литеры. Это означает, что формула B не выводима из множества формул A1, A2, …, An n.

2. В результате очередного применения правила резолюции получен пустой дизъюнкт. Это означает, что что формула B выводима из множества формул A1, A2, …, An.

3. Процесс зацикливается, т. е. получаются все новые и новые резольвенты, среди которых нет пустых. Это ничего не означает.

Пример 3.8.

В примере 3.3 а) был обоснован вывод A É (B É C), A& BC. Применим для этого примера метод резолюций. Для этого нужно проверить вывод

A É (B É C), A& B, Ø C„ .

Будем действовать в соответствии с алгоритмом.

Шаг 1. Нужно привести к КНФ формулы A É (B É C), A& B, Ø C.

A É (B É C) º Ø A V (B É C) º Ø A V Ø B V C.

Формулы A& B, Ø C уже находятся в КНФ.

Шаг 2. Составим множество S дизъюнктов:

S = {Ø A V Ø B V C, A, B, Ø C}.

Шаг 3. Построим резолютивный вывод из S. Для этого выпишем по порядку все дизъюнкты из S:

1) Ø A V Ø B V C;

2) A;

3) B;

4) Ø C;

Вместо пары дизъюнктов, содержащих контрарные литеры запишем их резольвенту (в скобках указаны номера формул, образующих резольвенту):

5) Ø B V C. (1, 2)

6) C. (3, 5)

7) . (4, 6)

Вывод заканчивается пустым дизъюнктом, что является обоснованием вывода A É (B É C), A& BC.

Пример 3.9.

Записать с помощью формул логики высказываний и решить методом резолюций следующую задачу:

«Чтобы хорошо учиться, надо прикладывать усилия. Тот, кто хорошо учится, получает стипендию. В данный момент студент прикладывает усилия. Будет ли он получать стипендию?

Введем следующие высказывания:

A = ”студент хорошо учится”.

B = ”студент прикладывает усилия”.

C = ”студент получает стипендию”

Чтобы утвердительно ответить на вопрос задачи: ”Будет ли студент получать стипендию? ”, нужно проверить вывод:

B É A, A É C, BC.

Будем действовать в соответствии с алгоритмом.

Шаг 1. Нужно привести к КНФ формулы B É A, A É C, B, Ø C.

B É A = Ø B V A,

A É C = Ø A VC,

Формулы B и Ø C уже находятся в КНФ.

Шаг 2. Составим множество S дизъюнктов:

S = {Ø B V A, Ø A VC, B, Ø C}.

Шаг 3. Построим резолютивный вывод из S. Сначала перепищем по порядку дизъюнкты из S:

1) Ø B V A.

2) Ø A VC.

3) B.

4) Ø C.

Затем вместо пары дизъюнктов, содержащих контрарные литеры запишем их резольвенту:

5) Ø B V C. (1, 2)

6) C. (3, 5)

7) . (4, 6)

Таким образом, на вопрос задачи можно ответить утвердительно: ”Студент будет получать стипендию”.

Правило резолюций более общее, чем правило modus ponens и производные правила, рассмотренные в п. 3.2. Докажем методом резолюций правило modus ponens. Необходимо построить вывод

A, A É BB.

Построим резолютивный вывод.

A, Ø A V BB.

A, Ø A V B, Ø B„ .

S = {A, Ø A V B, Ø B}.

1) A.

2) Ø A V B.

3) Ø B.

4) B. (1, 2)

5) . (3, 4)

Метод резолюций легко поддается алгоритмизации. Это позволяет использовать его в логических языках, в частности в ПРОЛОГе. Недостатком этого метода является необходимость представления формул в КНФ. Кроме того, автоматическое доказательство теорем методом резолюций основан на переборе и этот перебор может быть настолько большим, что затраты времени на него практически неосуществимы. Эти обстоятельства стимулируют поиски различных модификаций метода резолюций.

Приведем еще один пример применнения метода резолюций, основанного на попарном переборе дизъюнктов.

Пример 3.10.

Построим с плмощью метода резолюций следующий вывод:

Ø A É B, C V A, B É Ø CA,

Или, что то же:

Ø A É B, C V A, B É Ø C, Ø A „ .

Перепишем все посылки в виде дизъюнктов:

A V B, C V A, Ø B V Ø C, Ø A „ .

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

1) A V B

2) C V A

3) Ø B V Ø C

4) Ø A

5) A V Ø C (1, 3)

6) B (1, 4)

7) A V Ø B (2, 3)

8) C. (2, 4)

9) A (2, 5)

10) Ø C (3, 6)

11) Ø B (3, 8)

12) Ø C (4, 5)

13) Ø B (4, 7)

14)  (4, 9)

Мы видим, что такая стратегия перебора неэффективна. В данном случае существует более быстрый вывод. Например:

5) B. (1, 4)

6) C. (2, 4)

7) Ø B. (3, 6)

8) . (5, 7)

 

ТЕМА 4. НЕЧЕТКАЯ ЛОГИКА

Нечеткие множества

 

В 1965 году американский математик Лотфи Заде (L. Zade) опубликовал статью “Нечеткие множества” (“Fuzzy sets”). Было дано новое определение понятия множества, предназначенное для описания сложных плохо определенных систем, в которых наряду с количественными данными присутствуют неоднозначные, субъективные, качественные данные

Понятие множества лежит в основе всех математических конструкций, и статья Заде породила новое научное направление. Произошло “раздвоение” математики, появились нечеткие функции, нечеткие отношения, нечеткие уравнения, нечеткая логика и т. д. Эти понятия широко используются в экспертных системах, системах искусственного интеллекта. Изложим основные понятия нечетких множеств.

Определение 4.1. Нечетким множеством на множестве X назовем пару (X, mA), где mA(x) – функция, каждое значение которой mA(x) Î [0, 1] интерпретируется как степень принадлежности точки xÎ X множеству . Функция mA – называется функцией принадлежности множества .

Для обычного четкого множества A можно положить

mA(x) =

Таким образом, обычное множество является частным случаем нечеткого множества.

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

Пример 4.1.

Приведем пример нечеткого множества , которое формализует понятие " несколько", ясного лишь на интуитивном уровне.

Пусть X = {1, 2, 3, …, n, …} – множество натуральных чисел, а функция mA(x) задана таблицей:

 

x 1 2 3 4 5 6 7 8 9 10 …
mA(x) 0 0, 1 0, 6 0, 8 1 1 0, 9 0, 7 0, 2 0 …

 

Аналогично можно ввести понятия " много", " мало", " около 100", " почти 20", и т.д.

Переменные, значениями которых являются нечеткие множества, называются лингвистическими. Это основной тип переменных в языке людей.

Пример 4.2.

Пусть X = (0, ¥ ) – множество положительных чисел, а функция mA(x) задана формулой:

mA(x) =

График этой функции изображен на рис. 4.1.

Рис. 4.1

 

Если переменную x интерпретировать как возраст, то нечеткое множество соответствует понятию " старый". Аналогично можно ввести понятия " молодой", " средних лет" и т. д.

Пример 4.3.

Переменная " расстояние" принимает обычно числовые значения. Однако в предложениях естественного языка она может фигурировать как лингвистическая со значениями: " малое", " большое", " среднее", " около 5 км" и т. д. Каждое значение описывается нечетким множеством. Пусть речь идет о поездках на такси по городу. В качестве универсального множества X можно взять отрезок [0, 100] км и задать функцию принадлежности значений так, как показано на рис. 4.2.

Рис.4.2


Поделиться:



Последнее изменение этой страницы: 2017-03-14; Просмотров: 502; Нарушение авторского права страницы


lektsia.com 2007 - 2024 год. Все материалы представленные на сайте исключительно с целью ознакомления читателями и не преследуют коммерческих целей или нарушение авторских прав! (0.062 с.)
Главная | Случайная страница | Обратная связь