Системы искусственного интеллекта.
Курс лекций для студентов специальности 220200.
Основные направления ИИ.
Термин искусственный интеллект (ИИ) появился в 80-е годы ХХ века. Не существует единого и общепринятого определения ИИ. Это не удивительно, так как нет универсального определения человеческого интеллекта. К ИИ принято относить ряд алгоритмов и программных систем, которые могут решать некоторые задачи так как это делает человек. В 90-е годы в исследованиях по ИИ выделились шесть основных направлений [1].
Представление знаний. В рамках этого направления решаются задачи, связанные с формализацией и представлением знаний в памяти интеллектуальной системы (ИС). Для этого разрабатываются специальные модели представления знаний и языки для описания знаний, создаются процедуры и методы, с помощью которых ИС может приобретать знания. ИС – это система, функционирование которой опирается на знания о проблемной области, которые хранятся в ее памяти.
Манипулирование знаниями. В рамках данного направления строятся способы пополнения знаний на основе их неполных описаний, разрабатываются процедуры обобщения знаний и формирования на их основе абстрактных понятий, создаются методы достоверного и правдоподобного вывода на основе имеющихся знаний, предлагаются модели рассуждений, опирающихся на знания и имитирующих особенности человеческих рассуждений. Манипулирование знаниями тесно связано с представлением знаний. Теория баз знаний включает в себя проблемы, относящиеся к обоим направлениям.
Общение. В круг задач данного направления входят: проблема понимания связных текстов на ограниченном и неограниченном естественном языке, синтез связных текстов, понимание речи и синтез речи, теория моделей коммуникации между человеком и ИС. К этому направлению относится проблема формирования объяснения действий ИС, которые она должна уметь порождать по просьбе человека, а также комплекс задач, связанных с интеграцией в единый внутренний образ сообщений различной модальности ( речевых, текстовых, зрительных и т.п.), полученных в процессе коммуникации. На основе исследований в этом направлении формируются методы построения лингвистических процессоров, вопросно-ответных систем, диалоговых систем и других ИС, целью которых является обеспечение комфортных условий для общения человека с ИС.
Восприятие. Это направление традиционно включает: проблемы анализа трехмерных сцен, разработку методов представления информации о зрительных образах в базе знаний, создание методов перехода от зрительных сцен к их текстовому описанию и методов обратного перехода, создание средств порождения зрительных сцен на основе внутренних представлений в ИС.
Обучение. Предполагается, что ИС будут способны к обучению – решению задач, с которыми они ранее не встречались. Для этого необходимо создать методы формирования условий задачи по описанию проблемной ситуации или по наблюдению за этой ситуацией, научиться переходу от известных решений частных задач к решению общей задачи, создать методы декомпозиции исходной задачи на более мелкие, известные ИС, разработать модели самого процесса обучения, создать теорию подражательного поведения.
Поведение. Так как ИС должны действовать в некоторой окружающей среде, то необходимо разработать специальные поведенческие процедуры, которые позволили бы им адекватно взаимодействовать с окружающей средой, другими ИС и людьми. Для этого следует создать: модели целесообразного поведения, нормативного поведения, ситуативного поведения, специальные методы многоуровневого планирования и коррекции планов в динамических ситуациях.
Классификация СИИ.
На основе исследований в области искусственного интеллекта сформировалась новая область индустрии – производство интеллектуальных систем. Интеллектуальными системами называют такие автоматизированные системы, которые предназначены для реализации интеллектуальных задач, решаемых людьми.
К системам искусственного интеллекта относятся следующие типы автоматизированных систем:
Естественно- языковые системы;
Системы речевого общения;
Системы обработки визуальной информации;
Системы машинного перевода;
Экспертные системы и оболочки экспертных систем;
Все существующие интеллектуальные системы делятся на два класса:
Системы общего назначения;
Специализированные системы.
Системы общего назначения содержат метапроцедуры поиска, при помощи которых они генерируют и исполняют процедуры решения новых конкретных задач. Технология использования таких систем состоит в следующем. Пользователь (эксперт) формирует знания (данные и правила), описывающие выбранное приложение. Затем на основании этих знаний, заданной цели и исходных данных метапроцедуры системы генерируют и исполняют процедуру решения конкретной задачи. Данную технологию называют технологией инженерии знаний. Она позволяет специалисту, не знающему программирования, разрабатывать гибкие прикладные системы. В настоящее время, единственными системами общего назначения можно считать оболочки экспертных систем.
К специализированным относятся системы, которые выполняют решение фиксированного набора задач, предопределенного при проектировании интеллектуальной системы. Для использования таких систем требуется заполнить их данными, соответствующими выбранному приложению. В настоящее время многие специализированные интеллектуальные системы, в частности речевого общения и обработки изображений стали разрабатывать в виде экспертных систем.
Основными функциями естественно-языковых систем (ЕЯ-систем) являются: ведение диалога, понимание высказываний и генерация высказываний. Учитывая историю развития естественно-языковых систем, различают следующие классы ЕЯ-систем:
Интеллектуальные вопросно-ответные системы;
Системы общения с базами данных;
Диалоговые системы решения задач;
Системы обработки связных текстов.
Вопросно-ответные системы возникли в процессе развития информационно-поисковых систем, основное внимание при их разработке уделялось не столько их практическому использованию, сколько развитию моделей и методов, позволяющих осуществлять перевод ЕЯ-высказываний, относящимся к узким и заранее фиксированным областям, в формальное представление, а также обратный перевод.
Основной задачей создания систем общения с базами данных стало обеспечение доступа к информации в БД широкому классу неподготовленных конечных пользователей, которые формулируют запрос к БД на естественном языке.
Диалоговые системы решения задач помимо функций ЕЯ-доступа к БД, берут на себя решение заранее определенных классов задач (планирование боевых действий, путешествий, перевозок и т.д.). В этом случае разбиение задачи на подзадачи и распределение решения подзадач между участниками определяет не пользователь, а сама диалоговая система. Основным направлением практического использования ЕЯ-систем данного класса является реализация ЕЯ-общения с экспертными системами.
Системы обработки связных текстов предназначены для обработки больших объемов текстовой информацией для извлечения из нее каких-либо сведений.
Системы речевого общения предназначены для реализации ЕЯ-общения на основе устной речи. Узко специальные проблемы, стоящие перед такими системами – это создание преобразователей «текст – речевой сигнал» и «речевой сигнал – текст». Первая проблема – это проблема синтеза речи, вторая – анализа и распознавания речи.
Системы переработки визуальной информации решают три типа задач: обработка изображений (исходные данные и результаты обработки представлены в виде изображений), анализ изображений (входные данные являются изображением, а результат представляется в неизобразительной форме, например, в виде текста), синтез изображений (на входе имеется описание изображения, а на выходе по нему строится само изображение).
Системы машинного перевода предназначены для быстрого доступа к информации на иностранном языке, перевода больших потоков текстов. Процесс машинного перевода представляет собой последовательность преобразований, применяемых к входному тексту и превращающих его в текст на выходном языке, который должен максимально воссоздавать смысл и, как правило, структуру исходного текста, но уже средствами выходного языка.
Экспертные системы (ЭС) предназначены для решения неформализованных задач, то есть задач, решаемых с помощью неточных знаний, которые являются результатом обобщения многолетнего опыта работы и интуиции специалистов. Неформализованные знания обычно представляют собой эвристические приемы и правила. ЭС отличаются от традиционных систем программирования тем, что ориентированы на решение неформализованных задач и обладают следующими особенностями:
алгоритм решения не известен заранее, а строится самой ЭС с помощью символических рассуждений, базирующихся на эвристических приемах;
ясность полученных решений, то есть система «осознает» в терминах пользователя, как она получает решение;
способность анализа и объяснения своих действий и знаний;
способность приобретения новых знаний от пользователя-эксперта, не знающего программирования, и изменения в соответствии с ними своего поведения;
обеспечение «дружественного», как правило, естественно-языкового интерфейса с пользователем.
Обычно к ЭС относят системы, основанные на знании, то есть системы, вычислительная возможность которых является в первую очередь следствием их наращиваемой базы знаний (БЗ) и только во вторую очередь определяется используемыми методами. В настоящее время ЭС используются при решении задач следующих типов: принятие решений в условиях неопределенности (неполноты), интерпретация символов и сигналов, предсказание, диагностика, конструирование, планирование, управление, контроль и так далее.
Характеристики знаний.
Основной проблемой, решаемой в СИИ всех типов, является проблема представления знаний. Информация представляется в компьютере в процедурной и декларативной форме. В процедурной форме представлены программы, в декларативной – данные. В системах искусственного интеллекта возникла концепция новой формы представления информации – знания, которая объединила в себе черты как процедурной, так и декларативной информации. Перечислим основные характеристики знаний:
Внутренняя интерпретируемость. Каждая информационная единица должна иметь уникальное имя, по которому система находит ее, а также отвечает на запросы, в которых это имя упомянуто. Данные в памяти лишены имен и могут идентифицироваться только программой, извлекающей их из памяти. При переходе к знаниям в память вводится информация о некоторой протоструктуре информационных единиц и словари имен данных. Каждая единица информации будет экземпляром протоструктуры. СУБД обеспечивают реализацию внутренней интерпретируемости информации, хранимой в базе данных.
Структурированность. Информационные единицы должны соответствовать «принципу матрешки», то есть рекурсивной вложимости одних информационных единиц в другие. Другими словами, должна существовать возможность произвольного установления между отдельными информационными единицами отношений типа «часть – целое», «род – вид» или «элемент – класс».
Связность. Между информационными единицами должна быть предусмотрена возможность установления связей различного типа, характеризующих отношения между информационными единицами. Семантика отношений может носить декларативный характер как, например, в отношениях «одновременно» и «причина – следствие», или процедурный характер как, например, в отношении «аргумент – функция». Все отношения можно разделить на четыре категории: отношения структуризации (задают иерархию информационных единиц), функциональные отношения (несут процедурную информацию, позволяющую вычислять одни информационные единицы через другие), каузальные отношения (задают причинно-следственные связи) и семантические отношения (все остальные отношения).
Семантическая метрика. Между информационными единицами задают отношения релевантности, которые характеризуют ситуационную близость информационных единиц, то есть силу ассоциативной связи между информационными единицами (например, «покупка» или «регулирование движения на перекрестке»). Отношение релевантности позволяет находить знания, близкие к уже найденным.
Активность. Выполнение программ в информационных системах должно инициализироваться не командами, а состоянием информационной базы, например, появлением в базе фактов или описаний событий или установление связей между информационными единицами.
Перечисленные характеристики определяют разницу между данными и знаниями, при этом базы данных перерастают в базы знаний.
Модели представления знаний.
В интеллектуальных системах используются четыре основных типа моделей знаний:
Логические модели. В основе моделей такого типа лежит формальная система, задаваемая четверкой вида M = . Множество T есть множество базовых элементов, например слов из некоторого словаря, или деталей из некоторого набора. Для множества T существует некоторый способ определения принадлежности или непринадлежности произвольного элемента к данному множеству. Процедура такой проверки может быть любой, но она должна давать ответ на вопрос, является ли x элементом множества T за конечное число шагов. Обозначим эту процедуру P(T).
Множество S есть множество синтаксических правил. С их помощью из элементов T образуют синтаксически правильные совокупности. Например, из слов словаря строятся синтаксически правильные фразы, а из деталей собираются конструкции. Существует некоторая процедура P(S), с помощью которой за конечное число шагов можно получить ответ на вопрос, является ли совокупность X синтаксически правильной.
В множестве синтаксически правильных совокупностей выделяется некоторое подмножество A. Элементы A называются аксиомами. Как и для других составляющих формальной системы, должна существовать процедура P(A) , с помощью которой для любой синтаксически правильной совокупности можно получить ответ на вопрос о принадлежности ее к множеству A.
Множество B есть множество правил вывода. Применяя их к элементам A, можно получать новые синтаксически правильные совокупности, к которым снова можно применять правила из B. Так формируется множество выводимых в данной формальной системе совокупностей. Если имеется процедура P(B), с помощью которой можно определить для любой синтаксически правильной совокупности, является ли она выводимой, то соответствующая формальная система называется разрешимой. Это показывает, что именно правила вывода являются наиболее сложной составляющей формальной системы.
Для знаний, входящих в базу знаний, можно считать, что множество A образуют все информационные единицы, которые введены в базу знаний извне, а с помощью правил вывода из них выводятся новые производные знания. Другими словами, формальная система представляет собой генератор порождения новых знаний, образующих множество выводимых в данной системе знаний. Это свойство логических моделей позволяет хранить в базе лишь те знания, которые образуют множество A, а все остальные знания получать из них по правилам вывода.
Сетевые модели. Сетевые модели формально можно описать в виде H = 1, C2,…, Cn, G). Здесь I есть множество информационных единиц; C1, C2,…, Cn - множество типов связей между ними. Отображение G задает связи из заданного набора типов связей между информационными единицами, входящими в I.
В зависимости от типов связей, используемых в модели, различают классифицирующие сети, функциональные сети и сценарии. В классифицирующих сетях используются отношения структуризации. Такие сети позволяют в базах вводить иерархические отношения между информационными единицами. Функциональные сети характеризуются наличием функциональных отношений. Их часто называют вычислительными моделями, так как они позволяют описывать процедуры «вычислений» одних информационных единиц через другие. В сценариях используются каузальные отношения, а также отношения типа «средство – результат». Если в сетевой модели допускаются связи различного типа, то ее называют семантической сетью.
3.Продукционные модели. В моделях этого типа используются некоторые элементы логических и сетевых моделей. Из логических моделей заимствована идея правил вывода, которые здесь называются продукциями, а из сетевых моделей – описание знаний в виде семантической сети. В результате применения правил вывода к фрагментам сетевого описания происходит трансформация семантической сети за счет смены ее фрагментов, наращивания сети и исключения из нее ненужных фрагментов. Таким образом, в продукционных моделях процедурная информация явно выделена и описывается иными средствами, чем декларативная информация. Вместо логического вывода, характерного для логических моделей, в продукционных моделях появляется вывод на знаниях.
4.Фреймовые модели. В отличие от моделей других типов во фреймовых моделях фиксируется жесткая структура информационных единиц, которая называется протофреймом. В общем виде она выглядит следующим образом:
(Имя фрейма:
Имя слота 1 (значение слота 1)
Имя слота 2 (значение слота 2)
. . . . . . . . . . . . . .
Имя слота К (значение слота К)).
Значением слота может быть все, что угодно: числа, математические соотношения, тексты на естественном языке, программы, правила вывода, ссылки на другие слоты данного фрейма или других фреймов. В качестве значения слота может выступать набор слотов более низкого уровня, что позволяет реализовать во фреймовых представлениях «принцип матрешки».
При конкретизации фрейма ему и слотам присваиваются имена и происходит заполнение слотов. Таким образом, из протофреймов получаются фреймы-экземпляры. Переход от исходного протофрейма к фрейму-экземпляру может быть многошаговым, за счет постепенного уточнения значений слотов. Связи между фреймами задаются значениями специального слота с именем «Связь». Некоторые специалисты по ИС не выделяют фреймовые модели в отдельный класс, так как в ней объединены все основные особенности моделей остальных типов.
Исчисление высказываний.
Высказывание есть утвердительное предложение, которое либо истинно, либо ложно, но не то и другое вместе. Примеры высказываний: «Снег белый», «Прохоров – декан». «Истина» или «ложь», приписанная некоторому высказыванию, называется истинностным значением этого высказывания. Рассмотрим три истинных предложения:
За день до своей смерти он был еще жив;
Если верно, что когда идет дождь, то дорога мокрая, то справедливо также и следующее утверждение: если дорога сухая, то дождя нет;
Земля вертится.
Чтобы убедиться в правильности первого предложения, достаточно понимать смысл слов: это предложение является истиной языка. Чтобы принять второе утверждение, достаточно понимать смысл некоторых слов (если…то, нет), а также знать, что части фразы «идет дождь» и «дорога мокрая» являются высказываниями, которые могут быть истинными или ложными, однако все предложение останется истинным, если заменить эти два высказывания другими. Такие истины называются логическими истинами. Третье предложение выражает некоторый факт из физики и астрономии и является фактической истиной.
Исчисление высказываний – формальная логическая система. Множество ее базовых элементов составляют логический словарь (алфавит) T из бесконечного счетного множества высказываний, обозначаемых строчными латинскими буквами (иногда с индексами) и называемых атомами и пяти элементарных логических функций (связок):
«отрицание» -Ø, ~, -, not, не;
«конъюнкция» - Ù, &, and, и;
«дизъюнкция» - Ú, ÷, or, или;
«импликация» - ®, É, Þ;
«эквивалентность» - «, º, Û.
Словарь исчисления высказываний дает возможность строить составные высказывания из простых, соединяя их логическими связками. Правила построения S описывают выражения, являющиеся объектами языка. Такие высказывания называются формулами.
Совокупность правил построения формул выглядит так:
Всякий атом (высказывание) является формулой;
Если X и Y - формулы, то Ø X, (X Ù Y), (X Ú Y), (X ® Y) и (X « Y) – формулы;
Никаких формул, кроме порожденных применением указанных выше правил, нет.
Круглые скобки позволяют указать порядок, в котором применялись правила. Если в примере 2 утверждений, приведенных выше, обозначим высказывание «идет дождь» буквой P, а высказывание «дорога мокрая» буквой Q, то используя правила построения все утверждение записывается следующим образом:
(P ® Q) ®( ØQ ® ØP).
Объектами изучения естественных и формальных языков являются, в частности, синтаксис, который позволяет распознавать фразы среди наборов слов, и семантика, которая придает определенное значение фразам. Это относится и к исчислению высказываний. Любое высказывание может быть либо истинно, либо ложно. Введем семантическую область {И, Л}. Интерпретировать формулу это значит приписать ей одно из двух значений истинности: И или Л. Значение истинности формулы зависит только от стуктуры этой формулы и от значений истинности составляющих ее высказываний. Таблица истинности логических связок исчисления высказываний приведена ниже.
P |
Q |
Ø P |
P Ù Q |
P Ú Q |
P ® Q |
P « Q |
И |
И |
Л |
И |
И |
И |
И |
И |
Л |
Л |
Л |
И |
Л |
Л |
Л |
И |
И |
Л |
И |
И |
Л |
Л |
Л |
И |
Л |
Л |
И |
И |
Если формула состоит из нескольких атомов, то истинность формулы определяется при всех возможных комбинациях истинностных значениях атомов, встречающихся в формуле.
Рассмотрим формулу: (P Ù Q) ® (ØR). Таблица истинности для нее будет выглядеть следующим образом:
P |
Q |
R |
ØR |
P Ù Q |
(P Ù Q) ® (ØR) |
И |
И |
И |
Л |
И |
Л |
И |
И |
Л |
И |
И |
И |
И |
Л |
И |
Л |
Л |
И |
И |
Л |
Л |
И |
Л |
И |
Л |
И |
И |
Л |
Л |
И |
Л |
И |
Л |
И |
Л |
И |
Л |
Л |
И |
Л |
Л |
И |
Л |
Л |
Л |
И |
Л |
И |
Определение 1: интерпретацией формулы исчисления высказываний называется такое приписывание истинностных значений атомам формулы, при котором каждому из атомов приписано либо И, либо Л.
Определение 2: Формула истинна при некоторой интерпретации тогда и только тогда, когда она получает значение И в этой интерпретации, в противном случае формула ложна.
Определение 3: Формула является общезначимой (тавтологией) тогда и только тогда, когда она истинна при всех возможных интерпретациях. Формула является необщезначимой тогда и только тогда, когда она не является общезначимой.
Определение 4: Формула является противоречивой (невыполнимой) тогда и только тогда, когда она ложна при всех возможных интерпретациях. Формула является непротиворечивой (выполнимой) тогда и только тогда, когда она не является противоречивой.
Если Q - тавтология, то ее обозначают как ú= Q. Если E – множество формул, то запись E ú= Q означает, что при всех интерпретациях, при которых истинны все формулы из E, истинна также формула Q. Формула Q называется логическим следствием из E. Таким образом, тавтология – логическое следствие из пустого множества. Если E содержит единственный элемент P, то P ú= Q. Тогда Q является логическим следствием P тогда и только тогда, когда импликация P ® Q есть тавтология, или P ú= Q « ú= (P® Q). В более общем виде можно написать: { F1, F2,…, Fn } ú= Q « ú= (F1 Ù F2 Ù…Fn) ú= Q.
Определение 5: Пусть даны формулы F1, F2,…, Fn и формула Q. Говорят, что Q есть логическое следствие формул F1, F2,…, Fn тогда и только тогда, когда для всякой интерпретации I, в которой F1 Ù F2 Ù…Fn истинна, Q также истинна. F1, F2,…, Fn называются аксиомами ( или постулатами, или посылками, или гипотезами).
Если формулы P и Q – логические следствия друг друга, то они называются логически эквивалентными. Такая ситуация имеет место тогда и только тогда, когда формула (P « Q) является тавтологией. Понятие тавтологии совпадает с понятием теоремы в аксиоматической системе. Аксиоматическая система обладает свойством адекватности, то есть она состоит из множества аксиом, считающихся общезначимыми. Кроме аксиом в аксиоматическую систему входит множество правил вывода, позволяющих строить новые общезначимые выражения из аксиом и уже полученных общезначимых выражений. Выводимая формула обозначается ú¾ P.
Древнейшая из аксиоматических теорий – это Евклидова геометрия.
Исчисление высказываний тоже является аксиоматической системой. Любая аксиоматическая система должна удовлетворять следующим требованиям:
Непротиворечивость: невозможность вывода отрицания уже доказанного выражения (которое считается общезначимым);
Независимость (минимальность): система не должна содержать бесполезных аксиом и правил вывода. Некоторое выражение независимо от аксиоматической системы, если его нельзя вывести с помощью этой системы. В минимальной системе каждая аксиома независима от остальной системы, то есть не выводима из других аксиом.
Полнота (взаимность адекватности): любая тавтология выводима из системы аксиом. В адекватной системе аксиом любая выводимая формула есть тавтология, то есть верно, что ú¾ P® ú= P. Соответственно в полной систем верно: ú= P® ú¾ P.
Некоторое множество тавтологий составляет систему аксиом A. Приведем две наиболее известные системы аксиом, обладающие всеми вышеперечисленными свойствами.
Классическая система аксиом :
P ®( Q ® P);
(P ®( Q ® R))®(( P ® Q)®( P ® R));
(ØP ® Ø Q) ® ((ØP ® Q) ® P).
Система аксиом Новикова:
P ®( Q ® P);
(P ®( Q ®R))®(( P ® Q)®( P ® R));
P Ù Q ® P;
P Ù Q ® Q;
(P ® Q) ®(( P ® R) ®( P ® Q Ù R));
P ® P Ú Q;
Q ® P Ú Q;
(P ® R) ®(( Q ® R) ®( P Ú Q ® R));
(P ® Q) ®(Ø Q ®Ø P);
P ®ØØ P;
ØØ P ® P.
Существует три обязательных правила вывода, входящих в B в исчислении высказываний:
Все аксиомы выводимы.
Правило одновременной подстановки: если некоторая тавтология U содержит атом P, то одновременная замена всех вхождений атома P в U на любую формулу Q приводит к порождению тавтологии.
Modus Ponens (заключение): если P – тавтология, и P® Q, то Q – тавтология.
Можно доказать следующие дополнительные правила вывода:
Если P - тавтология, то Q ® P – тавтология (доказательство следует из аксиомы 1.1 и правила вывода 3).
Свойство транзитивности отношения следования: если P® Q, Q® R – тавтологии, то P® R – тавтология.
Обобщением правила 4 является теорема дедукции: необходимым и достаточным условием выводимости Q из гипотез R, P является выводимость P® Q из R. Данную теорему можно записать следующим образом: R, P ú¾ Q « R ú¾ (P® Q).
Определение 6. Выводом формулы P из формул U1, U2,…, Un называется последовательность формул F1, F2,…, Fn такая, что Fm есть P, а любая Fi либо аксиома, либо одна из формул Ui , либо формула, непосредственно выводимая из предшествующих ей формул.
Часто необходимо преобразовывать формулы из одной формы в другую. Поэтому, кроме аксиом и правил вывода необходимо иметь набор эквивалентных формул (законов), которые позволяют производить преобразования формул:
P « Q = P ® Q Ù Q ® P;
P ® Q = Ø P Ú Q;
Коммуникативные законы: P Ú Q = Q Ú P; P Ù Q = Q Ù P;
Ассоциативные законы: : (P Ú Q) Ú R = Q Ú (P Ú R); (P Ù Q) Ù R = Q Ù (P Ù R);
Дистрибутивные законы: P Ú (Q Ù R) = (P Ú Q) Ù (P Ú R);
P Ù (Q Ú R) = (P Ù Q) Ú (P Ù R);
Законы идемпотентности: P Ú P = P; P Ù P = P;
P Ú Л = P; P Ù И = P;
P Ú И = И; P Ù Л = Л;
P Ú ØP = И; P Ù ØP = Л;
Ø(ØP )= P;
Законы де Моргана: Ø(P Ú Q) = ØQ Ù ØP; Ø(P Ù Q) =ØQ Ú ØP;
Вследствие законов ассоциативности скобки в выражениях, связанных отношениями дизъюнкции и конъюнкции могут быть опущены, при этом выражение F1 Ú F2 Ú…Ú Fn называется дизъюнкцией формул F1, F2,…, Fn, а выражение F1 Ù F2 Ù…Ù Fn называется конъюнкцией формул F1, F2,…, Fn.
Определение 7. Литерал (литера) есть атом или отрицание атома.
Определение 8. Формула F находится в конъюнктивной нормальной форме тогда и только тогда, когда F имеет вид: F1 Ù F2 Ù…Ù Fn, n >=1, где каждая из F1, F2,…, Fn есть дизъюнкция литералов.
Определение 9. Формула F находится в дизъюнктивной нормальной форме тогда и только тогда, когда F имеет вид: F1 Ú F2 Ú…Ú Fn, n >=1, где каждая из F1, F2,…, Fn есть конъюнкция литералов.
Теорема 1. Пусть даны формулы F1, F2,…, Fn и формула P. Тогда P есть логическое следствие F1, F2,…, Fn тогда и только тогда, когда формула ((F1 Ù F2 Ù…Ù Fn)®P) общезначима.
Теорема 2. Пусть даны формулы F1, F2,…, Fn и формула P. Тогда P есть логическое следствие F1, F2,…, Fn тогда и только тогда, когда формула (F1 Ù F2 Ù…Ù Fn ÙØP) противоречива.
Теоремы 1 и 2 очень важны. Из них следует, что доказательство логического следствия одной формулы из конечного множества формул эквивалентно доказательству того факта, что некоторая связанная с конечным множеством формула общезначима или противоречива.
Исчисление предикатов первого порядка.
В логике высказываний атом рассматривается как единое целое, его структура и состав не анализируется. Однако, есть много умозаключений, которые не могут быть представлены таким простым способом. Например, рассмотрим следующее умозаключение:
Каждый человек смертен.
Так как Конфуций человек, то он смертен.
Приведенное рассуждение интуитивно корректно, однако, если мы введем обозначения:
P: Каждый человек смертен,
Q: Конфуций – человек,
R: Конфуций смертен,
то R не есть логическое следствие P и Q в рамках логики высказываний.
В логике предикатов первого порядка по сравнению с логикой высказываний имеет еще три логических понятия: термы, предикаты и кванторы.
Множество T базовых элементов исчисления предикатов включает в себя следующие символы:
Константы – это обычно строчные буквы a, b, c… или осмысленные имена объектов;
Переменные – это обычно строчные буквы x, y, z, …, возможно с индексами;
Функции – это обычно строчные буквы f, g, h,… или осмысленные слова из строчных букв;
Предикаты – это обычно прописные буквы P, Q, R … или осмысленные слова из прописных букв;
Логические связки: отрицание, дизъюнкция, конъюнкция, импликация, эквивалентность;
Кванторы всеобщности и существования - ", $;
Открывающая и закрывающая скобка.
Всякая функция или предикатный символ имеет определенное число аргументов. Если функция f имеет n аргументов, то f называется n- местной функцией. Аналогично, если предикат P имеет n аргументов, то P называется n- местным предикатом.
Определение 10. Термы определяются рекурсивно следующим образом:
Константа есть терм;
Переменная есть терм;
Если f есть n- местная функция и t1, t2,…,tn – термы, то f (t1, t2,…,tn) – терм;
Никаких термов, кроме порожденных применением указанных выше правил, нет.
Определение 11. Предикат P(t1, t2,…,tn) есть логическая функция, определенная на множестве термов t1, t2,…,tn, при фиксированных значениях которых она превращается в высказывания со значением истина (И) или ложь(Л).
Определение 12. Если P – n- местный предикат и t1, t2,…,tn – термы, то P(t1, t2,…,tn) – атом.
Для построения формул в исчислении предикатов используются пять логических связок и два квантора: " - всеобщности и $ - существования. Если x – переменная, то ("x) читается как «для всех x», «для каждого x», «для любого x», тогда как ($x) читается как « существует x», «для некоторых x», «по крайней мере для одного x».
Пример 1: запишем следующие утверждения:
Каждое рациональное число есть вещественное число.
Существует число, которое является простым.
Для каждого числа x существует такое число y , что x
Обозначим «x есть простое число» через P(x), «x есть рациональное число» через Q(x), «x есть вещественное число» через R(x) и «x меньше y» через МЕНЬШЕ (x, y).
Тогда указанные выше утверждения могут быть записаны соответственно выражениями:
("x) (Q(x)® R(x)),
($x) P(x),
("x) ($y) МЕНЬШЕ (x, y).
Каждое из выражений 1, 2, 3 называется формулой. Прежде чем дать формальное определение формулы в логике предикатов, следует установить различие между связанными переменными и свободными переменными и определить область действия квантора, входящего в формулу, как ту формулу, к которой этот квантор применяется. Так, область действия квантора существования в выражении 3 есть МЕНЬШЕ (x, y), а область действия квантора всеобщности в выражении 3 есть ($y) МЕНЬШЕ (x, y).
Определение 13. Вхождение переменной x в формулу называется связанным тогда и только тогда, когда оно совпадает с вхождением в квантор ("x) или ($y) или (и?) находится в области действия квантора. Вхождение переменной в формулу свободно тогда и только тогда, когда оно не является связанным.
Определение 14. Переменная свободна в формуле, если хотя бы одно ее вхождение в эту формулу свободно. Отметим, что переменная в формуле может быть свободной и связанной одновременно.
В формуле ("x) P(x,y)переменная x связана, так как оба вхождения x связаны, однако переменная y – свободна, так единственное вхождение y свободно.
Определение 15. Правильно построенные формулы логики первого порядка рекурсивно определяются следующим образом:
Атом есть формула.
Если F и G – формулы, то Ø(F), (F Ú G) , (F Ù G), (F®G), (F «G) – формулы.
Если F – формула, а x – свободная переменная в F, то ("x) F и ($x) F –формулы.
Формулы порождаются только конечным числом применений правил 1-3.
Определение 16. Терм t называется свободным для переменной x в формуле f, если ни x, ни другая произвольная переменная из t не находится в области действия никакого квантора "x или $x в f.
Пример2: переведем в формулу утверждение «Каждый человек смертен. Конфуций – человек, следовательно, Конфуций смертен».
Обозначим «x есть человек» через P(x), а «x смертен» через Q(x). Тогда утверждение «Каждый человек смертен» может быть представлено формулой ("x) (P(x)® Q(x)), утверждение «Конфуций – человек» формулой P(Конфуций) и «Конфуций смертен» формулой Q(Конфуций).
Утверждение в целом может быть представлено формулой
("x) (P(x)® Q(x))Ù P(Конфуций) ® Q(Конфуций).
Интерпретация формул в логике предикатов первого порядка.
Чтобы определить интерпретацию для формулы логики первого порядка, мы должны указать предметную область, значения констант, функций и предикатов, встречающихся в формуле.
Определение 17. Интерпретация формулы F логики первого порядка состоит из непустой (предметной) области D и указания значения всех констант, функций и предикатов, встречающихся в F.
Каждой константе мы ставим в соответствие некоторый элемент из D.
Каждой n- местной функции мы ставим в соответствие отображение из Dn в D (заметим, что Dn = {(x1, x2,…,xn)ç x1Î D, x2Î D,…, xnÎ D}).
Каждому n- местному предикату мы ставим в соответствие отображение Dn в {И, Л}.
Для каждой интерпретации формулы из области D формула может получить значение И или Л согласно следующим правилам:
Если заданы значения формул F и G, то истинностные значения формул Ø(F), (F Ú G) , (F Ù G), (F®G), (F «G) получаются с помощью таблиц истинности соответствующих логических связок.
("x) F получает значение И, если F получает значение И для каждого x из D , в противном случае она получает значение Л.
($x) F получает значение И, если F получает значение И хотя бы для одного x из D , в противном случае она получает значение Л.
Отметим, что формула, содержащая свободные переменные, не может получить истинностное значение. Поэтому, в дальнейшем, будем считать, что формула либо не содержит свободных переменных, либо свободные переменные рассматриваются как константы.
Пример 3. Рассмотрим формулы ("x) P(x) и ($x) ØP(x).
Пусть интерпретации такова: область - D={1,2};
Оценка для P :P(1) =И, P(2) =Л.
В таком случае ("x) P(x) есть Л, а ($x) ØP(x) есть И в данной интерпретации.
Пример 4. Рассмотрим формулы ("x) ($y) P(x, y).
Пусть интерпретации такова: область - D={1,2};
Оценка для P: P(1,1) =И, P(1,2) =Л, P(2,1) =Л, P(2,2) =И.
При x=1 существует y=1, что P(x, y) =И.
При x=2 существует y=2, что P(x, y) =И.
Следовательно, в указанной интерпретации, для каждого x из D существует такой y, что P(x, y)=И, то есть ("x) ($y) P(x, y) есть И в данной интерпретации.
Определение 18: Формула является непротиворечивой (выполнимой) тогда и только тогда, когда существует такая интерпретация I, что G имеет значение И в I. В этом случае говорят, что I удовлетворяет G.
Определение 19: Формула является противоречивой (невыполнимой) тогда и только тогда, когда не существует интерпретации, которая удовлетворяет G.
Определение 20: Формула G является общезначимой тогда и только тогда, когда не существует никакой интерпретации, которая не удовлетворяет формуле G.
Определение 21: Формула G есть логическое следствие формул F1, F2,…, Fn тогда и только тогда, когда для каждой интерпретации I, если F1 Ù F2 Ù…Fn истинна в I, то G также истинна в I.
Теоремы 1 и 2 верны также и для логики предикатов первого порядка.
Пример 5. Рассмотрим формулы:
F1: ("x) (P(x)® Q(x)),
F2: P(a).
Докажем, что Q(a) есть логическое следствие формул F1 и F2.
Рассмотрим любую интерпретацию I, которая удовлетворяет ("x) (P(x)® Q(x))Ù P(a). Конечно, в этой интерпретации P(a) есть И. Пусть Q(a) есть Л в данной интерпретации, тогда P(a)® Q(a) есть Л в данной интерпретации по определению операции импликации. Это значит, что ("x) (P(x)® Q(x)) есть Л в I, что невозможно. Следовательно, Q(a) должна быть И в каждой интерпретации, которая удовлетворяет ("x) (P(x)® Q(x))Ù P(a). Это означает, что Q(a) есть логическое следствие из F1 и F2.
Так как в логике первого порядка имеется бесконечное число областей, то имеется бесконечное число интерпретаций формулы. Следовательно, в отличие от логики высказываний, невозможно доказать общезначимость или противоречивость формулы оценкой формулы при всех возможных интерпретациях.
Системы аксиом логики предикатов.
Системы аксиом исчисления высказываний остаются верными и в исчислении предикатов первого порядка, только к ним следует добавить еще две аксиомы, которые дают возможность оперировать с кванторами:
("x) P(x)® P(y);
P(y) ®$ P(x).
Эти 2 аксиомы, добавленные в классическую систему аксиом или в систему аксиом Новикова, образуют системы аксиом, обладающие свойствами полноты, независимости и непротиворечивости.
Правила вывода в исчислении предикатов.
Из правил вывода исчисления высказываний в исчислении предикатов действует только правило Modus Ponens. Правило одновременной подстановки модифицировано, а остальные правила вывода касаются выводимости формул, содержащих кванторы.
Modus Ponens: Если выводима формула P и выводима формула P ®Q, то выводима и формула Q. Часто это правило записывают следующим образом:
P, P ®Q ;
Q
Правило одновременной подстановки: если терм t свободен для переменной x в формуле F, то можно подставить терм t вместо переменной x во всех вхождениях x в F.
Правило обобщения: если P не содержит свободных вхождений переменной x, то
P®Q(x) ;
P®"xQ(x)
Правило конкретизации: если P не содержит свободных вхождений переменной x, то
Q(x)®P ;
$xQ(x)®P
Правило переименования. Из выводимости формулы F(x), содержащей свободное вхождение х, ни одно из которых не содержится в области действия кванторов "y и $y следует выводимость F(y).
Пример 6. Докажем правило переименования:
+F(x);
Из аксиомы 2 классической системы следует, что
, где G – тавтология, не содержащая свободный вхождений x;
По правилу Modus Ponens следует, что
;
Используя правило обобщения, получаем:
;
По правилу Modus Ponens следует, что
;
Из аксиомы 2 логики предикатов и правила Modus Ponens следует, что
.
Предваренные (пренексные) нормальные формы исчисления предикатов.
В логике высказываний были введены две нормальные формы – КНФ и ДНФ. В логике предикатов также существуют нормальная форма - ПНФ, которая используется для упрощения процедуры доказательства общезначимости или противоречивости формул.
Определение 22: Формула F логики предикатов находится в предваренной нормальной форме, тогда и только тогда, когда формула F имеет вид:
(K1x1)…(Knxn) (M), где каждое (Kixi), i = 1,…,n, есть или ("xi) или ($xi), и M есть формула, не содержащая кванторов. (K1x1)…(Knxn) называется префиксом, а M – матрицей формулы F.
Законы эквивалентных преобразований логики предикатов.
Законы эквивалентных преобразований логики высказываний используются и в логике предикатов. Кроме них, существуют другие эквивалентные формулы, содержащие кванторы.
Пусть P есть формула, содержащая свободную переменную x. Пусть Q есть формула, которая не содержит переменной x. Тогда следующие пары эквивалентных формул являются законами эквивалентных преобразований логики предикатов:
("x) P(x)Ú Q=("x) (P(x)Ú Q);
("x) P(x)Ù Q=("x) (P(x)ÙQ);
($x) P(x)Ú Q=($x) (P(x)Ú Q);
($x) P(x)Ù Q=($x) (P(x)ÙQ);
Ø(("x) P(x))=( $x) (ØP(x));
Ø(($x) P(x))=( "x) (ØP(x));
("x) P(x)Ù ("x) Q(x)=("x) (P(x)ÙQ(x));
($x) P(x)Ú ($x) Q(x)=($x) (P(x)Ú Q(x));
Правила 7 и 8 называются правилами выноса кванторов, которые позволяют распределять квантор всеобщности и квантор существования по операциям конъюнкции и дизъюнкции соответственно. Следует отметить, что нельзя распределять квантор всеобщности и квантор существования по операциям дизъюнкции и конъюнкции соответственно, то есть не эквивалентны следующие пары формул:
("x) P(x) Ú ("x) Q(x)<>("x) (P(x) ÚQ(x));
($x) P(x) Ù ($x) Q(x)<>($x) (P(x) Ù Q(x));
В подобных случаях можно заменить связанную переменную x в формуле ("x) Q(x) на переменную z, которая не всречается в P(x), так как связанная переменная является лишь местом для подстановки какой угодно переменной. Формула примет вид: ("x) Q(x)= ("z) Q(z). Пусть z не встречается в P(x). Тогда
($x) P(x) Ù ($x) Q(x)= ($x) P(x) Ù ($z) Q(z)
=($x) ($z)( P(x) Ù Q(z)) по правилу 1.
Аналогично, можно написать
("x) P(x) Ú ("x) Q(x)= ("x) P(x) Ú ("z) Q(z)
=("x) ("z)( P(x) Ú Q(z)) по правилу 1.
В общем случае эти правила можно записать в следующем виде:
9.(K1x) P(x) Ú (K2x) Q(x)=(K1x) (K2z)( P(x) Ú Q(z));
10.(K3x) P(x) Ù (K4x) Q(x)=(K3x) (K4z)( P(x) Ù Q(z)),
где K1, K2, K3, K4 есть кванторы " или $, а z не входит в P(x).
Когда K1= K2=$ и K3= K4=", то необязательно переименовывать переменную x, можно прямо использовать правила 7 и 8.
Используя законы эквивалентных преобразований логики высказываний и логики предикатов, всегда можно преобразовать любую формулу в ПНФ.
Алгоритм преобразования формул в ПНФ.
Шаг 1. Используем законы законы 1 и 2 исчисления высказываний для того, чтобы исключить логические связки импликации и эквивалентности.
Шаг 2. Многократно используем закон двойного отрицания, законы де Моргана и законы 5 и 6 исчисления предикатов, чтобы внести знак отрицания внутрь формулы.
Шаг 3. Переименовываем связанные переменные, если это необходимо.
Шаг 4. Используем законы 1, 2, 3, 4, 7,8, 9 и 10 до тех пор, пока все кванторы не будут вынесены в самое начало формулы, чтобы получить ПНФ.
Пример 6. Приведем формулу ("x) P(x) ® ($x) Q(x) к ПНФ:
("x) P(x) ® ($x) Q(x)=Ø(("x) P(x))Ú ($x) Q(x)(по закону 1 логики высказываний)
=($ x)( Ø P(x)) Ú ($ x) ) Q(x)( по закону 5 логики предикатов)
=($ x)( Ø P(x) Ú Q(x))( по закону 8 логики предикатов), что и есть ПНФ исходной формулы.
Автоматизация доказательства в логике предикатов.
Поиск общей разрешающей процедуры для проверки общезначимости формул начал Лейбниц в XVII веке, затем был продолжен в начале XX века до тех пор, пока в 1936 году Черч и Тьюринг независимо не доказали, что не существует никакой общей разрешающей процедуры, никакого алгоритма, проверяющего общезначимость формул в логике предикатов первого порядка.
Тем не менее, существуют алгоритмы поиска доказательства, которые могут подтвердить, что формула общезначима, если она на самом деле общезначима (для необщезначимых формул эти алгоритмы, вообще говоря, не заканчивают свою работу).
Очень важный подход к автоматическому доказательству теорем был дан Эрбраном в 1930 году. По определению общезначимая формула есть формула, которая истинна при всех интерпретациях. Эрбран разработал алгоритм нахождения интерпретации, которая опровергает данную формулу. Однако, если данная формула действительно общезначима, то никакой интерпретации не существует и алгоритм заканчивает работу за конечное число шагов. Метод Эрбрана служит основой для большинства современных автоматических алгоритмов поиска доказательства.
Гилмор в 1959 году одним из первых реализовал процедуру Эрбрана. Его программа была предназначена для обнаружения противоречивости отрицания данной формулы, так как формула общезначима тогда и только тогда, когда ее отрицание противоречиво. Однако, программа Гилмора оказалась неэффективной и в 1960 году метод Гилмора был улучшен Девисом и Патнемом. Однако их улучшения оказалось недостаточным, так как многие общезначимые формулы логики предикатов все еще не могли быть доказаны на ЭВМ за разумное время.
Главный шаг вперед сделал Робинсон в 1965 году, который ввел так называемый метод резолюций, который оказался много эффективней, чем любая описанная ранее процедура. После введения метода резолюций был предложен ряд стратегий для увеличения его эффективности. Такими стратегиями являются семантическая резолюция, лок-резолюция, линейная резолюция, стратегия предпочтения единичных и стратегия поддержки.
Скулемовские стандартные формы.
Процедуры доказательства по Эрбрану или методу резолюций на самом деле являются процедурами опровержения, то есть вместо доказательства общезначимости формулы доказывается, что ее отрицание противоречиво. Кроме того, эти процедуры опровержения применяются к некоторой стандартной форме, которая была введена Девисом и Патнемом. По существу они использовали следующие идеи:
Формула логики предикатов может быть сведена к ПНФ, в которой матрица не содержит никаких кванторов, а префикс есть последовательность кванторов.
Поскольку матрица не содержит кванторов, она может быть сведена к конъюнктивной нормальной форме.
Сохраняя противоречивость формулы, в ней можно исключить кванторы существования путем использования скулемовских функций.
Алгоритм преобразования формулы в ПНФ известен. При помощи законов эквивалентных преобразований логики высказываний можно свести матрицу к КНФ.
Алгоритм преобразования формул в ДНФ и КНФ.
Шаг 1. Используем законы законы 1 и 2 исчисления высказываний для того, чтобы исключить логические связки импликации и эквивалентности.
Шаг 2. Многократно используем закон двойного отрицания, и законы де Моргана, чтобы внести знак отрицания внутрь формулы.
Шаг 3. Несколько раз используем дистрибутивные законы и другие законы, чтобы получить НФ.
Алгоритм преобразования формулы (K1x1)…(Knxn) (M), где каждое (Kixi), i = 1,…,n, есть или ("xi) или ($xi), и M есть КНФ в скулемовскую нормальную форму (СНФ) приведен ниже.
Алгоритм преобразования ПНФ в ССФ.
Шаг 1. Представим формулу в ПНФ (K1x1)…(Knxn) (M), где M есть КНФ. Пусть Kr есть квантор существования в префиксе (K1x1)…(Knxn), 1<=r<=n.
Шаг 2. Если никакой квантор всеобщности не стоит левее Kr – выберем новую константу c, отличную от других констант, входящих в M, заменим все xr в M на c и вычеркнем Krxr из префикса. Если K1,…Ki – список всех кванторов всеобщности, встречающихся в M левее Kr, 1< i выберем новый i –местный функциональный символ f, отличный от других функциональных символов, заменим все xr в M на f(x1, x2,…xi) и вычеркнем Krxr из префикса.
Шаг 3. Применим шаг 2 для всех кванторов существования в префиксе. Последняя из полученных формул есть скулемовская стандартная форма формулы. Константы и функции, используемые для замены переменных квантора существования, называются скулемовскими функциями.
Пример 7. Получить ССФ для формулы ($x)("y)("z)($u)("v)($w) (P(x, y, z, u, v, w).
В этой формуле левее ($x) нет никаких кванторов всеобщности, левее ($u) стоят ("y) и ("z), а левее ($w) стоят ("y), ("z) и ("v). Следовательно, мы заменим переменную x на константу a, переменную u - на двухместную f(y, z), переменную w - на трехместную функцию g(y, z, v). Таким образом, мы получаем следующую стандартную форму написанной выше формулы:
("y)("z)("v)(P(a, y, z, f(y, z), g(y, z, v)).
Определение 22: Дизъюнктом называется дизъюнкция литералов. Дизъюнкт, содержащий r литералов, называется r- литеральным дизъюнктом. Однолитеральный дизъюнкт называется единичным дизъюнктом. Если дизъюнкт не содержит никаких литералов, то он называется пустым дизъюнктом- ÿ . Так как пустой дизъюнкт не содержит литер, которые могли бы быть истинными при любых интерпретациях, то пустой дизъюнкт всегда ложен.
Определение 23: Множество дизъюнктов S есть конъюнкция всех дизъюнктов из S , где каждая переменная в S считается управляемой квантором всеобщности.
Вследствие последнего определения, ССФ может быть представлена множеством дизъюнктов.
Пример 8: ССФ ("x)((ØP(x, f(x))Ú R(x, f(x), g(x)))Ù (Q (x, g(x)) Ú R(x, f(x), g(x)))) представить в виде множества дизъюнктов.
{ØP(x, f(x))Ú R(x, f(x), g(x)), Q (x, g(x)) Ú R(x, f(x), g(x))}.
Теорема 3. Пусть S – множество дизъюнктов, которые представляют ССФ формулы F. Тогда F противоречива в том и только в том случае, когда S противоречиво.
На основании теорем 2 и 3 можно сделать вывод, что формула G является логическим следствием формулы F тогда, когда противоречива конъюнкция множества S и формулы ØG, то есть противоречива формула S1 Ù S2 Ù …Sn Ù ØG. Таким образом, если в множество S добавить негативный литерал ØG и доказать, что полученное множество противоречиво, то тем самым можно доказать выводимость G из множества S.
Метод резолюций.
Основная идея метода резолюций состоит в том, чтобы проверить, содержит ли множество дизъюнктов пустой дизъюнкт. Если множество содержит пустой дизъюнкт, то оно противоречиво (невыполнимо). Если множество не содержит пустой дизъюнкт, то проеряется следующий факт: может ли пустой дизъюнкт быть получен из данного множества. Множество содержит пустой дизъюнкт, тогда и только тогда, когда оно пустое. Если множество можно свести к пустому, то тем самым можно докахать его невыполнимость. В этом исостоит метод резолюций, который часто рассматривают как специальное правило вывода, используемое для порождения новых дизъюнктов из данного множества.
Метод резолюций в исчислении высказываний.
Определение 24:Если A атом, то литералы A и ØA контрарны друг другу, и множество { A, ØA } называется контрарной парой.
Отметим, что дизъюнкт есть тавтология, если он содержит контрарную пару.
Определение 25: Правило резолюций состоит в следующем:
Для любых двух дизъюнктов C1 и C2, если существует литерал L1 в C1, который контрарен литералу L2 в C2, то вычеркнув L1 и L2 из C1 и C2 соответственно и построив дизъюнкцию оставшихся дизъюнктов, получим резолюцию (резольвенту) C1 и C2.
Пример 9: рассмотрим следующие дизъюнкты:
C1: PÚ R,
C2: ØPÚ Q.
Дизъюнкт C1 имеет литерал P, который контрарен литералу ØP в C2. Следовательно, вычеркивая P и ØP из C1 и C2 соответственно, построим дизъюнкцию оставшихся дизъюнктов R и Q и получим резольвенту RÚ Q.
Важным своством резольвенты является то, что любая резольвента двух дизъюнктов C1 и C2 есть логическое следствие C1 и C2. Это устанавлисвается в следующей теореме.
Теорема 4. Пусть даны два дизъюнкта C1 и C2. Тогда резольвента C дизъюнктов C1 и C2 есть логическое следствие C1 и C2.
Если есть два единичных дизъюнкта, то их резольвента, если она существует, есть пустой дизъюнкт ÿ. Более существенно, что для невыполнимого множества дизъюнктов многократным применением правила резолюций можно породить ÿ.
Определение 26: Пусть S – множество дизъюнктов. Резолютивный вывод C из S есть такая конечная последовательность С1, C2,…, Ck дизъюнктов, что каждый Ci или принадлежит S или является резольвентой дизъюнктов, предшествующих Ci, и Ck=C. Вывод ÿ из S называется опровержением (или доказательством невыполнимости ) S.
Пример 10. Рассмотрим множество S:
ØPÚ Q,
Ø Q,
P.
Из 1 и 2 получим резольвенту
4. ØP.
Из 4 и 3 получим резольвенту
5. ÿ.
Так как ÿ получается из S применениями правила резолюций , то согласно теореме 4 ÿ есть логическое следствие S, следовательно S невыполнимо.
Метод резолюций является наиболее эффективным в случае применения его к множеству Хорновских дизъюнктов.
Определение 27: Фразой называется дизъюнкт, у которого негативные литералы размещаются после позитивных литералов в конце дизъюнкта.
Пример 11: Р1 ÚР2 Ú…Рn Ú ØN1 Ú ØN2…Ú ØNm
Определение 28: Фраза Хорна это фраза, содержащая только один позитивный литерал.
Пример 12: преобразовать фразу Хорна в обратную импликацию.
Р Ú ØN1 Ú ØN2…Ú ØNm
ØN1 Ú ØN2…Ú ØNm =Ø (N1 Ù N2 Ù…ÙNm)
P¬ (N1 Ù N2 Ù…ÙNm)
P¬ N1, N2,…Nm
При представлении дизъюнктов фразами Хорна негативные литералы соответствуют гипотезам, а позитивный литерал представляет заключение. Единичный позитивный дизъюнкт представляет некоторый факт, то есть заключение, не зависящее ни от каких гипотез. Часто задача состоит в том, что надо проверить некоторую формулу, называемую целью, логически выведенную из множества правил и фактов. Резолюция является методом доказательства от противного: исходя из фактов, правил и отрицания цели, приходим к противоречию (пустому дизъюнкту).
Метод резолюций в исчислении предикатов.
Правило унификации в логике предикатов.
Правило резолюций предполагает нахождение в дизъюнкте литерала, контрарного литералу в другом дизъюнкте. Для дизъюнктов логики высказываний это очень просто. Для дизъюнктов логики предикатов процесс усложняется, так как дизъюнкты могут содержать функции, переменные и константы.
Пример 13. Рассмотрим дизъюнкты:
C1: P(x)Ú Q(x),
C2: ØP(f(x))Ú R(x).
Не существует никакого литерала в C1, контрарного какому-либо литералу в C2. Однако, если подставить f(a) вместо x в C1 и a вместо x в C2, то исходные дизъюнкты примут вид:
C1’: P(f(a))Ú Q(f(a)),
C2’: ØP(f(a))Ú R(a).
Так как P(f(a)) контрарен ØP(f(a)), то можно получить резольвенту
C3’: Q(f(a))Ú R(a).
В общем случае, подставив f(x) вместо x в C1, получим
C1’’: P(f(x))Ú Q(f(x)).
Литерал P(f(x)) в C1’’ контрарен литералу ØP(f(x)) в C2. Следовательно, можно получить резольвенту
C3: Q(f(x))Ú R(x).
Таким образом, если подставлять подходящие термы вместо переменных в исходные дизъюнкты, можно порождать новые дизъюнкты. Отметим, что дизъюнкт C3 из примера 13 является наиболее общим дизъюнктом в том смысле, что все другие дизъюнкты, порожденные правилом резолюции будут частным случаем данного дизъюнкта.
Определение 29: Подстановка q– это конечное множество вида {t1/v1,…,tn/vn}, где каждая vi – переменная, каждый ti – терм, отличный от vi, все vi различны.
Определение 30: Подстановка q называется унификатором для множества {E1,…, Ek} тогда и только тогда, когда E1q=E2q=… Ekq. Множество {E1,…, Ek} унифицируемо, если для него существует унификатор.
Прежде чем применить правило резолюции в исчислении предикатов переменные в литералах необходимо унифицировать.
Унификация производится при следующих условиях:
Если термы константы, то они унифицируемы тогда и только тогда, когда они совпадают.
Если в первом дизъюнкте терм переменная, а во втором константа, то они унифицируемы, при этом вместо переменной подставляется константа.
Если терм в первом дизъюнкте переменная и во втором дизъюнкте терм тоже переменная, то они унифицируемы.
Если в первом дизъюнкте терм переменная, а во втором - употребление функции, то они унифицируемы, при этом вместо переменной подставляется употребление функции.
Унифицируются между собой термы, стоящие на одинаковых местах в одинаковых предикатах.
Пример 14. Рассмотрим дизъюнкты:
1. Q(a, b, c) и Q(a, d, l). Дизъюнкты не унифицируемы.
2. Q(a, b, c) и Q(x, y, z). Дизъюнкты унифицируемы. Унификатор - Q(a, b, c).
Определение 31: Унификатор s для множества {E1,…, Ek} будет наиболее общим унификатором тогда и только тогда, когда для каждого унификатора q для этого множества существует такая подстановка l, что q=s ° l, то есть q является композицией подстановок s и l.
Определение 32: Композицией подстановок s и l есть функция s ° l, определяемая следующим образом (s ° l) [t]=s[ l[t]], где t – терм, s и l - подстановки, а l[t] – терм, который получается из t путем применения к нему подстановки l.
Определение 33: Множество рассогласований непустого множества дизъюнктов {E1,…, Ek} получается путем выявления первой (слева) позиции, на которой не для всех дизъюнктов из E стоит один и тот же символ, и выписывания из каждого дизъюнкта терма, который начинается с счимвола, занимающего данную позицию. Множество термов и есть множество рассогласований в E.
Пример 15. Рассмотрим дизъюнкты:
{P(x, f(y, z)), P(x, a), P(x, g(h(k(x))))}.
Множество рассогласований состоит из термов, которые начинаются с пятой позиции и представляет собой множество {f(x, y), a, g(h(k(x)))}.
Алгоритм унификации для нахождения наиболее общего унификатора.
Пусть E – множество дизъюнктов, D – множество рассогласований, k – номер итерации, sk наиболее общий унификатор на k-ой итерации.
Шаг 1. Присвоим k=0, sk=e (пустой унификатор), Ek=E.
Шаг 2. Если для Ek не существует множества рассогласований Dk, то остановка: sk – наиболее общий унификатор для E. Иначе найдем множество рассогласований Dk.
Шаг 3. Если существуют такие элементы vk и tk в Dk, что vk переменная, не входящая в терм tk, то перейдем к шагу 4. В противном случае остановка: E не унифицируемо.
Шаг 4. Пусть sk+1=sk { tk / vk}, заменим во всех дизъюнктах Ek tk на vk.
Шаг5. K=k+1. Перейти к шагу 2.
Пример 16. Рассмотрим дизъюнкты:
E={P(f(a), g(x)), P(y, y)}.
E0=E, k=0, s0=e.
D0={f(a),y}, v0=y, t0=f(a).
s1=={f(a)/y}, E1={P(f(a), g(x)), P(f(a), f(a))}.
D1={g(x),f(a)}.
Нет переменной в множестве рассогласований D1.
Следовательно, алгоритм унификации завершается, множество E – не унифицируемо.
С помощью унификации можно распространить правило резолюций на исчисление предикатов. При унификации возникает одна трудность: если один их термов есть переменная x, а другой терм содержит x, но не сводится к x, унификация невозможна. Проблема решается путем переименования переменных таким образом, чтобы унифицируемые дизъюнкты не содержали одинаковых переменных.
Определение 34: Если два или более литерала (с одиниковым знаком) дизъюнкта C имеют наиболее общий унификатор s, то Cs - называется склейкой C.
Пример 16. Рассмотрим дизъюнкты:
Пусть C= P(x)Ú P(f(y))Ú ØQ(x).
Тогда 1 и 2 литералы имеют наиболее общий унификатор s = {f(y)/x}. Следовательно, Cs=P(f(y))Ú ØQ(f(y)) есть склейка C.
Определение 35: Пусть C1 и C2 – два дизъюнкта, которые не имеют никаких общих переменных. Пусть L1 и L2 - два литерала в C1 и C2 соответственно. Если L1 и ØL2 имеют наиболее общий унификатор s, то дизъюнкт (C1s - L1s) È (C2s - L2s) называется резольвентой C1 и C2.
Пример 17:Пусть C1= P(x)Ú Q(x) и C2= ØP(a)Ú R(x). Так как x входит в C1 и C2, то мы заменим переменную в C2 и пусть C2= ØP(a)Ú R(y). Выбираем L1= P(x) и L2=ØP(a). L1 и L2 имеют наиболее общий унификатор s={a/x}. Следовательно, Q(a)Ú R(y) – резольвента C1 и C2.
Алгоритм метода резолюций.
Шаг 1. Если в S есть пустой дизъюнкт, то множество невыполнимо, иначе перейти к шагу 2.
Шаг 2. Найти в исходном множестве S такие дизъюнкты или склейки дизъюнктов C1 и C2, которые содержат унифицируемые литералы L1 Î C1 и L2 Î C2. Если таких дизъюнктов нет, то исходное множество выполнимо, иначе перейти к шагу 3.
Шаг 3. Вычислить резольвенту C1 и C2 и добавить ее в множество S. Перейти к шагу 1.
Язык логического программирования ПРОЛОГ.
Проиллюстрируем принцип логического программирования на простом примере: запишем известный метод вычисления наибольшего общего делителя двух натуральных чисел – алгоритм Евклида в виде Хорновских дизъюнктов. При этом примем новую форму записи фразы Хорна, например ØPÙØQÙØRÙS будем записывать как S: - P, Q, R. Тогда алгоритм Евклида можно записать в виде трех фраз Хорна:
NOD (x, x, x): -.
NOD (x, y, z): - B (x, y), NOD (f (x, y), y, z).
NOD (x, y, z): -B (y, x), NOD (x, f (y, x), z).
Предикат NOD – определяет наибольший общий делитель z для натуральных чисел x и y, предикат B – определяет отношение «больше», функция f – определяет операцию вычитания. Если мы заменим предикат B и функцию f обычными символами, то фразы примут вид:
NOD (x, x, x): -.
NOD (x, y, z): - x>y), NOD (x- y), y, z).
NOD (x, y, z): -y>x), NOD (x, y- x), z).
Для вычисления наибольшего общего делителя двух натуральных чисел, например 4 и 6, добавим к описанию алгоритма четвертый дизъюнкт:
ÿ: - NOD (4, 6, z).
Последний дизъюнкт – это цель, которую мы будем пытаться вывести из первых трех дизъюнктов.
Основы языка программирования Пролог.
Объекты рассуждения в Прологе называются термами – синтаксическими объектами одной из следующих категорий
константы,
переменные,
функции (составные термы или структуры), состоящие из имени функции и списка аргументов-термов, имена функций начинаются со строчной буквы..
Переменная в Прологе служит для обозначения объекта на который нельзя сослаться по имени. Константа в Прологе служит для обозначения имен собственных и начинается со строчной буквы.
Переменные в Прологе предназначены для установления соответствия между термами предикатов, действующих в пределах одной фразы (предложения), а не местом памяти для хранения данных. Переменная начинается с прописной буквы или знаков подчеркивания. Область действия переменной – предложение.
Специальным знаком «_» обозначается анонимная переменная, которая используется тогда, когда конкретное значение переменной не существенно для данного предложения. Анонимные переменные не отличаются от обычных при поиске соответствий, но не принимают значений и не появляются в ответах. Различные вхождения знака подчеркивания означают различные анонимные переменные.
Предложение- это фраза Хорна, в которой посылки связаны между собой логическим «И», а дизъюнкты- логическим «ИЛИ».
Простейшим типом предложения является факт. Любой факт имеет соответствующее значение истинности и определяет отношение между термами.
Факт является простым предикатом, который записывается в виде функционального терма, например:
мать( мария, анна).
отец( иван, анна).
Точка, стоящая после предиката, указывает на то, что рассматриваемое выражение является фактом.
Вторым типом предложений Пролога является вопрос или цель. Цель – это средство формулировки задачи, которую должна решать программа. Простой вопрос (цель) синтаксически является разновидностью факта, например:
Цель: мать (мария, юлия).
В данном случае программе задан вопрос, является ли мария матерью юлии. Если необходимо задать вопрос, кто является матерью юлии, то цель будет иметь следующий вид:
Цель: мать( X, юлия).
Сложные цели представляют собой конъюнкцию простых целей и имеют следующий вид:
Цель: Q1, Q2,…,Qn, где запятая обозначает операцию конъюнкции, а Q1, Q2,…,Qn – подцели главной цели.
Конъюнкция в Прологе истинна только при истинности всех компонент, однако, в отличие от логики, в Прологе учитывается порядок оценки истинности компонент (слева направо).
Пример 18.
Пусть задана семейная БД при помощи перечисления родительских отношений в виде списка фактов:
мать( мария, анна).
мать(мария, юлия).
мать( анна, петр).
отец( иван, анна).
отец( иван, юлия).
Тогда вопрос, является ли иван дедом петра, можно задать в виде следующей цели:
Цель: отец( иван, X), мать(X, петр).
На самом деле БД Пролога включает не только факты, но и правила, которые представляют собой не множество, а список. Для получения ответа БД просматривается по порядку, то есть в порядке следования фактов и предикатов в тексте программы.
Цель достигнута, если в БД удалось найти факт или правило, который (которое) удовлетворяет предикату цели, то есть превращает его в истинное высказывание. В нашем примере первую подцель удовлетворяют факты отец( иван, анна). и отец( иван, юлия). Вторую подцель удовлетворяет факт мать( анна, петр). Следовательно, главная цель удовлетворена, переменная X связывается с константой анна.
Третьим типом предложения является правило.
Правила – это предложения вида
H: - P1, P2,…, Pn.
Символ «: -» читается как «если», предикат H называется заголовком правила, а последовательность предикатов P1, P2,…, Pn называется телом правила. Приведенное правило является аналогом хорновского дизъюнкта ØP1ÚØ P2,…,ÚØPn ÚH. Предикаты P1, P2,…, Pn часто назыавают посылками. Заголовок следует из тела правила. Заголовок истинен, если истинны все посылки в теле правила. В посылках переменные связаны квантором существования, а в заголовке - квантором всеобщности.
Пример 19.
Добавим в БД примера 18 правила, задающие отношение «дед»:
мать( мария, анна).
мать(мария, юлия).
мать( анна, петр).
отец( иван, анна).
отец( иван, юлия).
дед (X, Y): - отец(X, Z), мать(Z, Y).
дед (X, Y): - отец(X, Z), отец(Z, Y).
Тогда вопрос, является ли иван дедом петра, можно задать в виде следующей цели:
Цель: дед( иван, петр).
Правила - самые общие предложения Пролога, факт является частным случаем правила без правой части, а цель – правило без левой части.
Очень часто правила в Прологе являются рекурсивными. Например, для нашей семейной БД предикат «предок» определяется рекурсивно:
предок(x, y): - мать(x, y).
предок(x, y): - отец(x, y).
предок(x, y): - мать(x, z), предок(z, y).
предок(x, y): - отец (x, z), предок(z, y).
Рекурсивное определение предиката обязательно должно содержать нерекурсивную часть, иначе оно будет логически некорректным и программа зациклится. Чтобы избежать зацикливания, следует также позаботиться о порядке выполнения предложений, поэтому практически полезно, а порой и необходимо придерживаться принципа: «сначала нерекурсивные выражения».
Программа на Прологе - это конечное множество предложений.
Использование дизъюнкции и отрицания.
Чистый Пролог разрешает применять в правилах и целях только конъюнкцию, однако, язык, используемый на практике, допускает применение дизъюнкции и отрицания в телах правил и целях. Для достижения цели, содержащей дизъюнкцию, Пролог–система сначала пытается удовлетворить левую часть дизъюнкции, а если это не удается, то переходит к поиску решения для правой части дизъюнкции. Аналогичные действия производятся при выполнении тела правил, содержащих дизъюнкцию. Для обозначения дизъюнкции используется символ « ; ».
В Прологе отрицание имеет имя «not» и для представления отрицания какого-либо предиката P используется запись not(P). Цель not(P) достижима тогда и только тогда, когда не удовлетворяется предикат (цель) P. При этом переменным значения не присваиваются. В самом деле, если достигается P, то не достигается not(P), значит надо стереть все присваивания, приводящие к данному результату. Наоборот, если P не достигается, то переменные не принимают никаких значений.
Область действия имен.
В Прологе программист свободен в выборе имен констант, переменных, функций и предикатов. Исключения составляют резервированные имена и числовые константы. Переменные от констант отличаются первой буквой имени: у констант она строчная, у переменных - заглавная.
Область действия имени представляет собой часть программы, где это имя имеет один и тот же смысл:
для переменной областью действия является предложение (факт, правило или цель), содержащее данную переменную;
для остальных имен (констант, функций или предикатов) – вся программа.
Алгоритмы Пролога.
Общий принцип выполнения программ на Прологе прост: производится поиск ответа на вопросы, задаваемые БД, состоящей из фактов и правил, то есть проверяется соответствие предикатов вопроса предложениям из БД. Это частный случай метода резолюций. Однако, результаты проводимого поиска нужно анализировать во вполне определенном порядке, применяя для проверки соответствий специальные функции Пролога, делающие его языком программирования. Наиболее примечательной из этих функций является отсечение. Основные принципы для получения ответа на заданный вопрос следующие:
в задаваемом вопросе допускается только один предикат, он и является целью, удовлетворяемой предложением из БД;
если цель есть атомарный предикат, то она удовлетворяется либо фактом, в том случае, когда он соответствует цели; либо правилом, в том случае, когда его заголовок соответствует цели, а предикаты, входящие в тело, могут стать истинными при присваивании термов некоторым переменным;
если цель представляет собой конъюнкцию предикатов, то она удовлетворяется, когда посредством присваивания термов переменным, будут последовательно (в текстуальном порядке) удовлетворены все входящие в цель предикаты.
Отметим, что в Прологе не проводится синтаксического различия между предикатом и функцией (составным термом), а также между нечисловой константой и функцией без аргументов. Следовательно, суть действия состоит в том, что ищется попарное соответствие между термами, один из которых является целью, а другой принадлежит БД.
Унификация переменных.
Установление соответствия между термами является основной операцией при вычислении цели. Она осуществляется следующим образом: на каждом шаге выбирается очередной терм и отыскивается соответствующее выражение в БД. При этом переменные получают или теряют значения. Этот процесс можно описать в терминах текстуальных подстановок: « подставить терм t вместо переменной Y». Свободными переменными в Прологе называются переменные, которым не были присвоены значения, а все остальные переменные называются связанными переменными. Переменная становится связанной только во время унификации, переменная вновь становится свободной, когда унификация оказывается неуспешной или цель оказывается успешно вычисленной. В Прологе присваивание значений переменным выполняется внутренними подпрограммами унификации. Переменные становятся свободными, как только для внутренних подпрограмм унификации отпадает необходимость связывать некоторое значение с переменной для выполнения доказательства подцели.
Правило унификации.
Если x и y-константы, то они унифицируемы, только если они равны.
Если x- константа или функция, а Y-переменная, то они унифицируемы, при этом Y принимает значение x .
Если x и y -функции, то они унифицируемы тогда и только тогда, когда у них одинаковые имена функций (функторы) и набор аргументов и каждая пара аргументов функций унифицируемы.
Есть особый предикат «=», который используется в Турбо-Прологе для отождествления двух термов. Использование оператора «=» поможет лучше понять процесс означивания переменной. В Турбо-Прологе оператор «=» интерпретируется как оператор присваивания или как оператор проверки на равенство в зависимости от того, являются ли значения термов свободными или связанными.
Пример 20: X=Y, если X и Y – связанные переменные, то производится проверка на равенство, например: если X=5 и Y=5, то результат ДА (истина); если X=6 а Y=5, то результат НЕТ(ложь). Если одна из переменных X или Y – свободная, то ей будет присвоено значение другой переменной, для Турбо-Пролога несущественно слева или справа от знака «=» стоит связанная переменная.
Оператор «=» ведет себя точно так, как внутренние подпрограммы унификации при сопоставлении целей или подцелей с фактами и правилами программы.
Вычисление цели. Механизм возврата.
Каноническая форма цели (вопроса) является конъюнкцией атомарных предикатов, то есть последовательностью подцелей, разделенных запятыми:
Q=Q1, Q2,…, Qn.
Пролог пытается вычислить цель при помощи унификации термов предикатов подцелей с соответствующими элементами в фактах и заголовках правил. Унификация выполняется слева направо. Некоторые подцели при унификации с некоторыми фактами или правилами могут оказаться неуспешными, поэтому Прологу требуется способ запоминания точек, в которых он может продолжить альтернативные поиски решения. Прежде чем реализовать один из возможных путей вычисления подцели, Пролог фактически помещает в программу указатель, который определяет точку, в которую может быть выполнен возврат, если текущая попытка будет неудачной.
Если некоторая подцель оказывается неуспешной, то Пролог возвращается влево и останавливается у ближайшего указателя возврата. С этой точки Пролог начинает попытку найти другое решение для неуспешной цели. До тех пор, пока следующая цель на данном уровне не будет успешной, Пролог будет повторять возврат к ближайшему указателю возврата. Эти попытки выполняются внутренними подпрограммами унификации и механизмом возврата.
Алгоритм вычисления цели – частный случай правила резолюции применительно к дизъюнктам Хорна. Вопрос Q является правилом без заголовка, аналогом выражения ØQ, то есть Q®Л. Пусть D – база данных (множество дизъюнктов). На вопрос Q, следует найти такую подстановку s, для которой множество s[DÈ(ØQ)] невыполнимо. Стратегия выбора очередной пары дизъюнктов для резолюции здесь очень проста: подцели и предложения просматриваются в текстуальном порядке.
Пример 21: пусть есть БД семья:
мать (екатерина, юлия).
мать (екатерина, анастасия).
мать (мария, петр).
мать (анна, екатерина).
отец (петр, юлия).
отец (петр, анастасия).
отец (антон, петр).
отец (андрей, екатерина).
дед (X, Y): - отец(X, Z), мать(Z, Y).
дед (X, Y): - отец(X, Z), отец(Z, Y).
бабка (X, Y): - мать(X, Z), мать(Z, Y).
бабка (X, Y): - мать(X, Z), отец(Z, Y).
Зададим сложную цель:
Q1, Q2 = отец(X, Y), мать(екатерина, Y).
Подцель Q1= отец(X, Y) соответствует пятому предложению БД :отец (петр, юлия). Это дает подстановку s1={X=петр, Y=юлия}. Затем найденная подстановка применяется к s1[Q2]= мать(екатерина, юлия). Этой подцели соответствует 1 предложение БД, что дает пустую подцель, следовательно ответ найден: X=петр, Y=юлия.
Для получения нового ответа в БД ищется новая унификация для s1[Q2]. Так как в БД нет соответствующего предложения, то вычисления прекращаются, система вновь рассматривает последовательность Q1, Q2 и для Q1 ищется новая унификация в БД, начиная с 6 предложения. Это и есть возврат. Шестое предложение сразу же дает желаемую унификацию с подстановкой s2={X=петр, Y=анастасия}. Вновь найденная подстановка применяется к s1[Q2]= мать(екатерина, анастасия). Этой подцели соответствует 2 предложение БД. Далее указанная процедура повторяется и в итоге имеем:
Цель: отец(X, Y), мать(екатерина, Y).
2 решения: X=петр, Y=юлия
X=петр, Y=анастасия.
Структура программ Турбо-Пролога.
Программа, написанная на Турбо-Прологе, состоит из пяти основных разделов: раздел описания доменов, раздел базы данных, раздел описания предикатов, раздел описания предложений и раздел описания цели. Ключевые слова domains, database, predicates, clauses и goal отмечают начала соответствующих разделов. Назначение этих разделов таково:
следующая страница >>
Смотрите также:
