Скачать 1.15 Mb.
|
Определение 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)}
v0 = y и t0 = f(a);
{Q(f(a), g(x), Q(f(a), f(a))};
Примеры. В заключение параграфа рассмотрим несколько примеров применения метода резолюций в исчислении высказываний (Пример 1) и в исчислении предикатов (Примеры 2,3). Пример 1. Даны 4 утверждения: ![]() ![]() ![]() ![]() Преобразуем все утверждения в стандартную форму: (1) ![]() ![]() ![]() ![]() Докажем путем опровержения, что ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Пример 2. Дано множество формул: ![]() ![]() ![]() ![]() Доказать, что ![]() ![]() ![]() ![]() ![]() (1) ![]() (2) ![]() ![]() (3) ![]() (4) O ![]() ![]() (5) ![]() ![]() Это множество дизьюнктов невыполнимо. Докажем при помощи метода резолюций: (6) ![]() (7) ![]() (8) □ резольвента (7) и (6). Т.о ![]() ![]() ![]() |
![]() | Конспект лекций по дисциплине "Программное обеспечение интеллектуальных систем". Для магистров специальности 5А521902 Целью данного курса является приобретение знаний по разработки и реализации основных элементов систем искусственного интеллекта | ![]() | Лабораторная работа №1 по дисциплине “Системы искусственного интелекта Исчисление предикатов первого порядка является теоретической основной множества формализмов методов искусственного интеллекта. Задачи... |
![]() | «шаг за шагом» создание искусственного интеллекта гашева Светлана Интеллект рассматривают как прикладную область исследований, связанных с имитацией отдельных функций интеллекта человека [6]. Распознавание... | ![]() | Учебно-методический комплекс по дисциплине “основы искусственного интеллекта” ... |
![]() | «Основы искусственного интеллекта» Рабочая учебная программа по дисциплине «Основы искусственного интеллекта» для ооп «050100 Физика и информатика по циклу б в. 13... | ![]() | Рабочая программа дисциплины «Системы искусственного интеллекта» Рабочая программа основана на требованиях Федерального государственного стандарта высшего профессионального образования по направлению... |
![]() | Учебно-методический комплекс по дисциплине “основы искусственного интеллекта” для специальности ... | ![]() | Учебно-методический комплекс по дисциплине “основы искусственного интеллекта” для специальности ... |
![]() | В. К. Финн к структурной когнитологии: феноменология сознания с точки зрения искусственного интеллекта Ки и искусственного интеллекта – полигона экспериментальной проверки научных средств имитации рациональности и продуктивного мышления.... | ![]() | 1. интеллектуальные системы Системы искусственного интеллекта, решающие задачи по обработке знаний и при этом проявляющие черты, сходные с чертами естественного... |