Конспект лекций по дисциплине «Системы искусственного интеллекта»




НазваниеКонспект лекций по дисциплине «Системы искусственного интеллекта»
страница5/11
Дата05.09.2012
Размер1.15 Mb.
ТипКонспект
1   2   3   4   5   6   7   8   9   10   11

Определение 5.4. Если Аатомная формула, то две литеры А и А называют контрарными, а множество {A , А}контрарной парой.


Заметим, что если дизъюнкт содержит контрарную пару, то он является тавтологией. .Если дизъюнкт не содержит литер, то он называется пустым дизъюнктом, если он содержит одну литеру, то называется однолитерным дизъюнктом, а если содержит к литер – к-литерным дизъюнктом. Так как пустой дизъюнкт не содержит литер, которые могли бы быть истинны, то он всегда ложен. Пустой дизъюнкт обозначается .

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

Справедлива следующая

Теорема 5.1. Пусть S – множество дизъюнктов, представляющих Скулемовскую стандартную форму формулы F. Тогда F противоречива в том и только в том случае, когда S противоречиво.

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

Далее для множеств дизъюнктов будут использованы термины невыполнимо/выполнимо вместо противоречиво/непротиворечиво.



Метод резолюций для исчисления высказываний.

Основная идея метода резолюций состоит в том, чтобы проверить, содержит ли множество S пустой дизъюнкт . Если S содержит пустой дизъюнкт, то, как следует из предыдущего параграфа, S невыполнимо. Если S не содержит , то проверяется: может ли  быть получен из S? Метод резолюций можно рассматривать как специальное правило вывода, используемое для порождения из S новых дизъюнктов. Это правило вывода таково:

в том случае, если для любых двух дизъюнктов C1и C2 существует литера L1 в С1, которая контрарна литере L2 в С2 то, вычеркнув L1 и L2, из C1 и C2 , соответственно, можно построить дизъюнкцию оставшихся дизъюнктов, которая будет являться следствием С1 и С2. Эта последняя дизъюнкция называется резольвентой. Корректность этого правила вывода устанавливает следующая

Т
еорема 5.2.
Пусть даны два дизъюнкта С1 и С2. Тогда резольвента С дизъюнктов С1 и С2 есть логическое следствие С1 и С2.

Д
оказательство.
Пусть





г
де Сa и Сb – дизъюнкции литер. Предположим, что С1 и С2 истинны в некоторой интерпретации I. Очевидно, либо L, либо L ложно в I. Пусть, например, L ложно в I. Тогда Сa должен быть истинен в I (иначе предположение об истинности С1 неверно). Таким образом, резольвента, т.е.


и
стинна в I. Аналогично можно показать, что если L ложно в I, то Сb должен быть истинен в I. Следовательно,


истинна в I, что требовалось доказать.

Пример 2.2.1.Рассмотрим множество дизъюнктов






Пример 2.2.2. Рассмотрим множество дизъюнктов





Из 1.и 2. получаем


4.


Из 3. и 4.получаем пустой дизъюнкт .


Лекция 6. Автоматизация дедуктивных рассуждений. Метод резолюций для исчисления предикатов первого порядка.

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





В С1 не существует литеры, контрарной какой-либо литере из С2. Однако, вспоминая, что все переменные в формулах P(x) и Q(x) имеют универсальную квантификацию и, подставляя f(x) в С1 вместо х, получим





Э
ти два дизъюнкта уже легко резольвировать; получим:


Если в С1 и С2 подставлять на места переменных другие подходящие термы, можно получать новые резольвенты С. Например, подставив a вместо х в С2 и f(a) вместо х в С1, получим резольвенту


Т

аким образом, резольвента

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

Из сказанного видно, что, получение резольвент из дизъюнктов часто требует подстановок.

6.1. Подстановки и унификация.

Определение 6.1. Подстановка – это конечное множество вида {t1/v1, …,t n/vn}, где каждая v i – переменная, а каждый ti – терм, отличный от vi и все vi различны. Подстановка, которая не содержит элементов, называется пустой и обозначается .

Определение 6.2. Пусть  = {t1/v1, …,t n/vn} – подстановка и Е –выражение. Тогда Е - выражение, полученное из Е одновременной заменой всех вхождений переменной vi на терм ti.

Е называют примером Е.

Определение 6.3. Подстановка  называется унификатором для множества

{E1,E2,…,E k } тогда и только тогда, кода E1 = E2=…= Ek. Если для множества Е существует унификатор, то оно называется унифицируемым.

Определение 6.4. Унификатор  для множества {E1,E2,…,E k } будет наиболее общим унификатором тогда и только тогда, когда для каждого унификатора  этого множества найдется такая подстановка , что =

Пример. Множество {P(a,y), P(x,f(b))} унифицируемо, так как подстановка  = {a/x, f(b)/y} является его унификатором.

Таким образом, ключевой задачей метода резолюций для исчисления предикатов первого порядка является нахождение наиболее общего унификатора. Прежде чем переходить к изложению общего алгоритма её решения дадим определение множества рассогласований.

Определение 6.5. Множество рассогласований непустого множества выражений W есть такое множество подвыражений, которые начинаются с различающихся символов, находящихся в одних и тех же позициях в выражениях из W.

Пример. 2.2.3. Если W = {P(x, f(y, z)), P(x, a), P(x, g(h(k(x))))}, то первой позицией, в которой появляются различные символы, является пятая (символы P(x, первых четырех позиций во всех выражениях из W совпадают); таким образом, множеством рассогласований будет являться множество W = {f(y, z), a, g(h(k(x)))}.


6.2. Алгоритм унификации.

Перейдем теперь к алгоритму унификации:


Алгоритм унификации.

Шаг 1. Положим k=0, Wk= W и  k= .

Шаг 2. Если Wk – единичный дизъюнкт, то k–наиболее общий унификатор для W. В противном случае – поиск множества Dk рассогласований для Wk.;

Шаг 3. Если существуют такие элементы vk и t k в Dk, что vk - переменная, не входящая в t k, то перейти к п.4.

Иначе W не унифицируемо;

Шаг 4. Пусть k+1=k{tk / vk} тогда Wk+1= W k{tk / vk};

Шаг 5. k := к+1; переход к п. 2.


Приведем некоторые примеры применения унификации.

Пример 1. Пусть W = {Q(f(a), g(x)), Q(y, y)}

  1. Положим 0 =  и W0 = W;

  2. Множество рассогласований для W0 – D0 = {f(a), y}, т.е.

v0 = y и t0 = f(a);

  1. Тогда 1=0{t0 / v0} = {f(a)/y} = {f(a)/y};

  2. W1= W0{ t0 / v0} = {Q(f(a), g(x), Q(y, y)} {f(a)/y}=

{Q(f(a), g(x), Q(f(a), f(a))};

  1. Множество рассогласований для W1 – D1= {g(x), f(a)},

  2. Так как подстановки, исключающей последнее рассогласование не существует, то множество W не унифицируемо.

  1. Пример 2. Пусть W={P(x,f(y)), P(a,u)}. На первом проходе алгоритма будет найдена подстановка 1= a/x , так как множество рассогласований D0={x,a}. Множество W1 будет равно {P(a,f(y)),P(a,u)}. На втором проходе алгоритма подстановка будет расширена до 2={ a/x, f(y)/u)} и W2={P(a,f(y))}. Так как W2 состоит из одного литерала, то алгоритм закончит работу и выдаст s2.

  2. Пример 3. Пусть W={P(x,f(y)), P(a,b)}. На первом проходе алгоритма будет найдена подстановка 1= a/x и W1={P(a,f(y)), P(a,b)}. На третьем шаге второго прохода будет выдано сообщение о том, что множество W неунифицируемо, так как множество рассогласования D1={f(y),a} не содержит переменной.

  3. Отметим, что при выполнении шага 4 из множества Wk удаляется одна из переменных (переменная vk), а никакой новой переменной не возникает. Это означает, что алгоритм унификации всегда заканчивает работу. Ясно также, что если алгоритм заканчивает работу на шаге 3, то множество М неунифицируемое. Также понятно, что если алгоритм заканчивает работу на шаге 2, то k – унификатор множества W.

  4. Таким образом, возвращаясь, собственно, к методу резолюций, получаем следующую схему применения метода в случае исчисления предикатов первого порядка:

  1. Взятие отрицания исходной формулы;

  2. Приведение формулы к Сколемовской нормальной форме;

  3. Нахождение унифицирующих подстановок и унификация множества дизъюнктов формулы;

  4. Резольвирование множества дизъюнктов и нахождение пустого дизъюнкта (если таковой существует).


Примеры.

В заключение параграфа рассмотрим несколько примеров применения метода резолюций в исчислении высказываний (Пример 1) и в исчислении предикатов (Примеры 2,3).

Пример 1. Даны 4 утверждения:









Преобразуем все утверждения в стандартную форму:

(1) 







Докажем путем опровержения, что  - логическое следствие из (1), (2) и (3). Отрицаем (4) и получаем: 





 отрицание заключения,

 резольвента (3) и (1),

резольвента (5) и (2),

 резольвента (6) и (4).


Пример 2. Дано множество формул:

 





Доказать, что  является логическим следствием  и . Преобразуем  и в стандартную форму и подучим следующие пять дизьюнктов:

(1)

(2)  из 

(3) 
(4) O из 
(5)  из 
Это множество дизьюнктов невыполнимо. Докажем при помощи метода резолюций:

(6)  резольвента (3) и (2),

(7)  резольвента (5) и (4),

(8) □ резольвента (7) и (6).

Т.о - логическое следствие  и .

1   2   3   4   5   6   7   8   9   10   11

Похожие:

Конспект лекций по дисциплине «Системы искусственного интеллекта» iconКонспект лекций по дисциплине "Программное обеспечение интеллектуальных систем". Для магистров специальности 5А521902
Целью данного курса является приобретение знаний по разработки и реализации основных элементов систем искусственного интеллекта
Конспект лекций по дисциплине «Системы искусственного интеллекта» iconЛабораторная работа №1 по дисциплине “Системы искусственного интелекта
Исчисление предикатов первого порядка является теоретической основной множества формализмов методов искусственного интеллекта. Задачи...
Конспект лекций по дисциплине «Системы искусственного интеллекта» icon«шаг за шагом» создание искусственного интеллекта гашева Светлана
Интеллект рассматривают как прикладную область исследований, связанных с имитацией отдельных функций интеллекта человека [6]. Распознавание...
Конспект лекций по дисциплине «Системы искусственного интеллекта» iconУчебно-методический комплекс по дисциплине “основы искусственного интеллекта”
...
Конспект лекций по дисциплине «Системы искусственного интеллекта» icon«Основы искусственного интеллекта»
Рабочая учебная программа по дисциплине «Основы искусственного интеллекта» для ооп «050100 Физика и информатика по циклу б в. 13...
Конспект лекций по дисциплине «Системы искусственного интеллекта» iconРабочая программа дисциплины «Системы искусственного интеллекта»
Рабочая программа основана на требованиях Федерального государственного стандарта высшего профессионального образования по направлению...
Конспект лекций по дисциплине «Системы искусственного интеллекта» iconУчебно-методический комплекс по дисциплине “основы искусственного интеллекта” для специальности
...
Конспект лекций по дисциплине «Системы искусственного интеллекта» iconУчебно-методический комплекс по дисциплине “основы искусственного интеллекта” для специальности
...
Конспект лекций по дисциплине «Системы искусственного интеллекта» iconВ. К. Финн к структурной когнитологии: феноменология сознания с точки зрения искусственного интеллекта
Ки и искусственного интеллекта – полигона экспериментальной проверки научных средств имитации рациональности и продуктивного мышления....
Конспект лекций по дисциплине «Системы искусственного интеллекта» icon1. интеллектуальные системы
Системы искусственного интеллекта, решающие задачи по обработке знаний и при этом проявляющие черты, сходные с чертами естественного...
Разместите кнопку на своём сайте:
Библиотека


База данных защищена авторским правом ©lib.znate.ru 2014
обратиться к администрации
Библиотека
Главная страница