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

Здравствуйте гость!

Задание № 2067

Наменование:

Курсовик Интеллектуальные информационные технологии

Предмет:

Информатика

Бюджет:

0 руб.

Дата:

26.11.2010

Описание:

Работа сделана, нужно её доделать, срочно! Работа готова, надо доделать готовую работу по рецензии.. Стоимость Ваша... Задание высылаю, работу готовую и рецензию при связи!

СОДЕРЖАНИЕ

Введение 5
1 Представление задач теоремами и доказательство теорем методом резолюции 7
1.1 Исчисление высказываний 7
1.2 Исчисление предикатов 21
1.3 Логическое представление 38
2 Концептуальные графы и продукционные модели 47
2.1 Концептуальные графы 47
2.1.1 Концептуальные графы семантических представлений 48
2.1.2 Представление вершин-отношения с N ребрами 49
2.1.3 Понятие ТИП и ЧИСЛОВОЙ МАРКЕР в концептуальных графах 50
2.1.4 Операции с концептуальными графами 51
2.2 Продукционные модели 54
3 Представление и использование нечётких знаний 57
3.1 Ненадежные знания и выводы 57
3.1.1 Разбиение задач с ненадежными данными 58
3.1.2 Метод MYCIN 60
3.1.3 Субъективный байесовский метод 64
3.1.4 Метод выводов на основе теории Демпстера-Шафера 69
3.1.5 Нечеткая логика 73
3.1.6 Вероятностная логика 74
3.2 Нечеткие множества и выводы 77
3.2.1 Обозначение нечетких множеств и функция принадлежности 77
3.2.2 Нечеткие отношения 80
3.2.3 Нечеткие выводы 83
4 Нейронные сети и использование оболочки ЭС 86
4.1 Описание теории 86
4.2 Описание задания 96
5 Лабораторные работы 101
5.1 Лабораторная работа № 1 101
5.2 Лабораторная работа № 2 108
5.3 Лабораторная работа № 3 111
5.4 Лабораторная работа № 4 114
6 Курсовой проект 128
6.1 Организация курсового проекта 128
6.1.1 Цели курсового проекта 128
6.1.2 Структура и содержание курсового проекта 128
6.2 Темы курсовых проектов 135
6.3 Требования к оформлению и содержанию курсового проекта 136
Список литературы 138
Приложение А 140
Приложение Б 141









ВВЕДЕНИЕ

Наиболее значительными работами в области искусствен-ного интеллекта являются разработки мощных компьютерных систем под названием интеллектуальные информационные сис-темы или экспертные системы, то есть системы, основанные на знаниях. Такие программы решения задач с представлением и применением фактических и эвристических знаний, с совмест-ной работой экспертов, инженеров по знаниям, разработчиков систем и логическим выводом позволяют переходить к новой информационной технологии, к новой технологии программи-рования.
Цель учебного методического пособия — сформулировать представления о ключевых концепциях построения интеллекту-альных информационных систем, моделях представления зна-ний, методах логического вывода, стратегиях разрешения кон-фликта и приобретение студентами умения и навыков использо-вания и создания на компьютере таких систем на основе логиче-ских рассуждений, механизмов вывода, зашумленных данных.
В результате изучения дисциплины, студенты должны знать:
• модели представления знаний;
• основные методы логического вывода;
• основные стратегии механизма вывода и разрешения конфликтного множества.
В результате изучения дисциплины, студенты должны уметь:
• поставить задачу, структурировать её;
• выбрать структуру базы знаний и данных;
• реализовать стратегии логического вывода;
• использовать для нечетких знаний выбранный метод не-четкого рассуждения.
Для изучения дисциплины «Интеллектуальные информаци-онные системы» студенты должны усвоить следующие дисцип-лины: теория вероятности, дискретная математика, базы дан-ных, программирование, информационные системы.
Структурно учебное методическое пособие состоит из шести разделов. В первых четырех рассматриваются теоретиче-ские аспекты, в пятом — задания четырёх лабораторных работ, в шестом — курсовой проект (работа).


1 ПРЕДСТАВЛЕНИЕ ЗАДАЧ ТЕОРЕМАМИ И ДОКАЗАТЕЛЬСТВО ТЕОРЕМ МЕТОДОМ РЕЗОЛЮЦИИ

1.1 Исчисление высказываний

Словарь, синтаксис, семантика
Исчисление высказываний [1, 8, 14, 16] изучает предложе-ния, которые могут быть либо истинными, либо ложными. Рас-смотрим три следующих истинных предложения (утверждения):
• За четверть часа до своей смерти он был еще жив.
• Если верно, что когда идет дождь, то дорога мокрая, то справедливо также и следующее утверждение: если дорога су-хая, то дождя нет.
• Земля вертится.
Чтобы убедиться в правильности первого предложения, достаточно понимать смысл слов: это предложение является ис-тиной языка. Чтобы принять второе утверждение, достаточно понимать смысл некоторых слов (если ... то, нет), а также знать, что куски фразы «идет дождь» и «дорога мокрая» являются вы-сказываниями, т.е. предложениями, которые могут быть истин-ными или ложными. Второе предложение останется истинным, если заменить эти два высказывания другими. Такие истины языка называются логическими истинами. Напротив, третье предложение не является истиной языка, так как оно выражает некоторый факт (в данном случае — из физики и астрономии). Таким образом, это предложение — фактическая истина.
Пропозициональный логический словарь традиционно со-ставляется из бесконечного счетного множества высказываний, обозначаемых строчными буквами (иногда с индексами), и пяти связок (точнее, логических или пропозициональных, связок), описанных в таблице на рис. 1.1.
Высказывания представляют собой предложения, которые могут быть истинными или ложными.
Теперь займемся логикой высказываний как таковой, т.е. безотносительно к ее связям с фразами естественного языка. В таком контексте логику высказываний часто называют исчисле-нием высказываний.
Название Обычное обо-значение Тип Другие обо-значения
Отрицание
Унарный - , ~, not, не
Конъюнкция
Бинарный &, . , and, и
Дизъюнкция
Бинарный |, or, или
Импликация
Бинарный ,

Эквивалентность
Бинарный , , ~


Рис. 1.1 — Логические связки.

Словарь исчисления высказываний дает возможность стро-ить сложные, или составные, высказывания из исходных (про-стых, элементарных), соединяя последние связками. Правила построения описывают те выражения, которые являются объек-тами языка. Такие высказывания называют формулами. Анало-гия с естественными языками очевидна: фраза — это составное высказывание, построенное по определенным правилам.
Совокупность правил построения выглядит так:
• Базис: всякое высказывание является формулой.
• Индукционный шаг: если X и Y — формулы, то X, (X Y), (X Y), (X Y) и (X Y) — формулы.
• Ограничение: формула однозначно получается с помо-щью правил, описанных в базисе и индукционном шаге.
Эта грамматика требует некоторых пояснений. Прежде все-го, появились два новых типа символов: X, Y и (,). Круглые скобки позволяют указать порядок, в котором применялись пра-вила построения. Например, в формуле
(1.1)
индукционный шаг применялся дважды: первый раз — при по-строении формулы из формул q и r, а второй — при по-строении заключительной формулы из формул p и . Скобки здесь использовались так же, как и в арифметике. Есте-ственность употребления скобок является следствием древовид-ности структуры логических формул и арифметических выра-жений. Описанное в базисе правило сопоставляет высказывания висячим узлам дерева, а индуктивное правило, сформулирован-ное в индукционном шаге, порождает дерево, растущее из неко-торого узла (связки) и построенное на основе одного из двух ранее сформированных деревьев (рис. 1.2). Корневой узел (ко-рень) дерева высказываний, соответствующего некоторой фор-муле, является связкой. Ее называют главной связкой формулы. Формула, у которой главная связка — импликация (эквивалент-ность), иногда называется условной (биусловной).



Рис. 1.2 — Древовидная форма формулы (1.1).

Естественным образом вводятся и прописные буквы X и Y. Это метасимволы, т.е. не принадлежащие языку обозначения, позволяющие вводить понятия и свойства этого языка. Буквы р, q, r представляют определенные высказывания. Метасимволы X и Y служат для обозначения формул вообще.
Уже отмечалось, что высказывание либо истинно, либо ложно. Поэтому введем семантическую область (И, Л}. Интер-претировать формулу — значит приписать ей одно из двух зна-мений истинности И или Л (часто используют обозначения 1 для И и 0 для Л).
Семантика (то есть набор правил интерпретации формул) должна быть композиционной: значение формулы должно быть функцией значений ее составляющих. Точнее: значение истин-ности формулы зависит только от структуры этой формулы и от значений истинности составляющих ее высказываний.
Таким образом, связки исчисления высказываний представ-ляют функции истинности: например, значение истинности формулы (X Y) будет известно, если известны значения ис-тинности X и Y. Рис. 1.2 описывает семантику отрицания. Се-мантика бинарных связок дана на рис. 1.2.
Интерпретация — это отображение i, сопоставляющее каж-дому элементарному высказыванию р некоторое значение истин-ности. Интерпретацию i, заданную на множестве элементарных высказываний, можно распространить (продолжить) на множест-во формул (высказываний) посредством таблиц истинности. Со-ответствующее продолжение (расширение) I тоже называется ин-терпретацией. Интерпретация, при которой истинное значение формулы есть И, называется моделью этой формулы.
Литера — это элементарное высказывание или его отри-цание. Литеры р и р противоположны. Интерпретация опре-деляет разбиение множества L литер на два подмножества LИ и Lл, каждое из которых содержит по одному элементу из каждой пары противоположных литер.
В исчислении высказываний имеется пять связок. С одной стороны, ясно, что для этих связок имеются «эквиваленты» в естественном языке. С другой стороны, естественный язык был бы сильно обеднен сокращением числа его связок до пяти. Ис-числение высказываний не станет богаче, если ввести дополни-тельные связки.
В естественном языке связки «не», «и», «или», «если ..., то» на первый взгляд вполне однозначно описываются приведенны-ми выше функциями истинности. Например, фразы
Хорошая погода или идет дождь
и
Идет дождь или хорошая погода (1.2)
кажутся синонимами. Однако иначе обстоит дело с фразами
Ему стало страшно и он убил чужака
и
Он убил чужака и ему стало страшно,
так как слово «и» подчеркивает здесь определенный временной и причинный нюанс. Наконец, многочисленные связки естест-венного языка ни в коей мере не соответствуют функциям ис-тинности. Связка «потому что» служит хорошим тому приме-ром. Чтобы убедиться в этом, предположим, что идет дождь (высказывание р) и что земля мокрая (высказывание q). Легко принимается как истинное высказывание
q потому что р,
но нельзя считать истинным высказывание
р потому что q.
Логическая дизъюнкция является неразделительной: она истинна, если истинным является хотя бы один из двух ее опе-рандов. В естественном языке союз «или» иногда является ис-ключающим (разделительным). В предложении «целое число четно или нечетно» одна ветвь альтернативы истинна, а другая ложна.
Импликация — очень важная связка; она отражает структу-ру рассуждений, в частности математических. Первый ее опе-ранд называется посылкой (или антецедентом), а второй — за-ключением (или консеквентом). Ясно, что если посылка истин-на, то импликация принимает значение истинности заключения. Однако может вызвать удивление, что импликация бывает ис-тинна и тогда, когда ее посылка ложна. Тем не менее легко убе-диться, что импликация (как мы ее определили) является един-ственной связкой, удовлетворяющей следующим требованиям:
• Если первый операнд истинный, то значение истин-ности совпадает со значением второго операнда.
• Значение истинности зависит от двух операндов.
• Связка некоммуникативна.
В той мере, в какой эти три критерии удачно очерчивают естественную импликацию, принятое нами определение служит наилучшим возможным приближением. Чтобы подчеркнуть этот нюанс, смоделированную связкой импликацию иногда назы-вают материальной импликацией. Материальная импликация — основная связка в математических рассуждениях. Она соединяет условие H и утверждение Т в теореме. Однако было бы незакон-но писать Н Т так как Н и Т — не логические формулы, а ка-кие-то достаточно произвольные высказывания: неформальные или принадлежащие некоторому нелогическому формализму. В таких случаях лучше писать Н=>Т. Аналогично, в таком контек-сте лучше писать С1<=>С2, а не С1 = С2.
Исчисление высказываний выражает только чисто функ-ционально-истинностные связи между высказываниями. Это очень хорошо, однако желательно иметь возможность выражать все многообразие взаимосвязей. Кроме того, нет особых причин ограничиваться унарными и бинарными связками.
Связка (функционально-истинностная) задается своей таб-лицей истинности. Таблица для связки с п операндами имеет 2n строк. С каждой из этих строк связано свое значение истин-ности. Таким образом, можно задать -арных (то есть с п опе-рандами) связок. Однако на самом деле двух связок и дос-таточно для порождения всех этих многочисленных связок при любых значениях п.
Три другие традиционные связки могут быть «определены» с помощью отрицания и импликации посредством следующих всегда истинных формул:

(1.3)

(Здесь центральная связка понимается как символ, обо-значающий «равенство по определению».)
С другой стороны, легко показать, что каждую n-арную связку можно определить (выразить, описать) через пять тради-ционных связок. Приведем пару расхожих примеров (как на ес-тественном языке, так и на математическом). Формула

задает исключающую дизъюнкцию X и Y. Далее, высказывание «если X, то Y, иначе Z» описывается формулой

соответствующей часто употребляемой тернарной связке. Отме-тим еще, что связками с нулевым числом операндов являются только И и Л. Их можно также считать n-арными связками для всех натуральных значений п.
Заметим, наконец, что бинарная связка «не-и», обозначае-мая , позволяет определить все другие связки. По определе-нию (X Y) ложно, только если X и Y истинны. В частности, эквивалентно X. Это свойство порождать все другие связки используется в цифровой электронике. Имея логические схемы, реализующие «не-и», можно построить любую логиче-скую схему, моделирующую заданную функцию истинности (и соответствующую ей связку). Связка «не-или», обозначаемая , является еще одной бинарной связкой, порождающей все другие связки. По определению (X Y) истинно тогда и только тогда, когда X и Y ложны.

Выполнимые и общезначимые формулы

Сейчас мы рассмотрим формулы, которые истинны при всех интерпретациях, а также формулы, которые при всех ин-терпретациях ложны. В дальнейшем это подведет нас к опреде-лению логического следствия.
Формула семантически выполнима или просто выполнима, если она допускает некоторую модель, т.е. ее можно интерпре-тировать со значением И. Например, формулы и выполнимы: они истинны, в частности, если р и q истинны. Другие примеры: все высказывания выполнимы, отрицания высказываний тоже выполнимы. Формула, не являющаяся выпол-нимой, называется невыполнимой. Формула невыпол-нима.
Формула общезначима, если она истинна, независимо от истинностных значений, приписанных составляющим ее выска-зываниям. Формула общезначима так же, как и формулы , и . Форму-лу, которая не является общезначимой, иногда называют необ-щезначимой.
Сразу же заметим, что отрицание общезначимой формулы — невыполнимая формула. Точно так же отрицание выполнимой формулы — необщезначимая формула. Иногда нейтральной на-зывают формулу, которая не является ни общезначимой, ни не-выполнимой.
Общезначимые формулы исчисления высказываний часто называют тавтологиями. Если А — формула, то запись
|= A
означает, что А есть тавтология. Более общо: если Е — множе-ство формул, то запись
E |= A
означает, что при всех интерпретациях, при которых истинны все формулы из Е, истинна также формула А. Формула А называется логическим следствием из Е. Таким образом, тавтология — логи-ческое следствие из пустого множества. Если Е содержит един-ственный элемент В, то пишут B |= A вместо {B} |= A. Легко ус-танавливается следующее утверждение: А является логическим следствием из В тогда и только тогда, когда материальная им-пликация есть тавтология (это остается верным, в част-ности, если В невыполнима или А общезначима). Данный ре-зультат можно записать так:

В более общем виде имеем

В этом контексте формулы Hi — называют гипотезами, а формулу С — заключением. Фундаментальная проблема логики, называемая проблемой дедукции, состоит в следующем: определить, является ли формула С логическим следствием множества формул Е. Мы только что видели, что, когда множе-ство Е конечно, проблема дедукции сводится к определению некоторой условной общезначимости. Определение, которое мы сейчас введем, позволит заняться проблемой дедукции эффек-тивнее.
Множество формул Е семантически выполнимо (или просто выполнимо), если все его элементы допускают общую модель; в противном случае оно невыполнимо. Таким образом, множество формул уподобляется (с точки зрения семантики) конъюнкции своих элементов.
Формула С является логическим следствием конечного мно-жества Е тогда и только тогда, когда невыполнимо. В этом состоит принцип дедукции. Заметим также, что множество Е невыполнимо тогда и только тогда, когда Л — его логическое следствие. Или еще можно сказать, что любая формула — его логическое следствие. Символически принцип дедукции запи-сывается следующим образом:

Если формулы А и В — логические следствия друг друга, то они называются логически эквивалентными. Такая ситуация имеет место тогда и только тогда, когда формула (А В) являет-ся тавтологией.

Дизъюнкты и нормальные формы

Как будет продемонстрировано в нашем изложении, бывает полезно преобразовать данную формулу в эквивалентную ей, имеющую вид «нормальной», или «канонической», формы. В этом отношении особый интерес представляют понятия «дизъ-юнкт» и «конъюнктивная нормальная форма».
Дизъюнктом называется дизъюнкция конечного числа ли-тер, то есть формула вида

Ее часто записывают как или просто как множество литер:
Такое представление является исключением из правила: дизъюнкт эквивалентен дизъюнкции (а не конъюнкции) своих элементов. По этой причине нужно каждый раз явно оговари-вать, что множество литер представляет именно дизъюнкт.
Пустой дизъюнкт — единственный невыполнимый дизъ-юнкт. Естественно его обозначить через Л.
Конъюнктивной нормальной формой (КНФ) называется конъюнкция конечного числа дизъюнктов.
Теорема 1.1. Любая формула имеет логически эквивалентную ей КНФ.
Доказательство. Ниже приведен алгоритм нормализации.
• Сначала заменяем на , а за-тем — на . Это делается для исключения свя-зок и .
• Необходимое число раз применяются правила преобра-зования, выведенные из законов де Моргана:
,
.
Символ — означает «заменяется на». В настоящем кон-тексте правило означает только . Двойные отри-цания «гасятся» по закону
.
На этой стадии связка «отрицание» остается только непо-средственно перед высказываниями.
• Наконец, необходимое число раз применяются правила преобразования, выведенные из законов дистрибутивности:
,
.
Формула, полученная в конце третьего этапа, это и есть нормальная форма, эквивалентная исходной формуле.
Дизъюнкты, содержащие противоположные литеры (то есть высказывание и его отрицание), общезначимы и могут быть опущены. Можно также опускать повторения литер в пределах одного и того же дизъюнкта. Полученная таким способом нор-мальная форма называется приведенной.
Алгоритм нормализации формулы очень прост, но, вообще говоря, неэффективен.
Если в некоторой нормальной форме дизъюнкт сi содержит-ся в дизъюнкте cj, то cj можно опустить. В частности, содержа-щую пустой дизъюнкт нормальную форму можно заменить этим единственным дизъюнктом.
Пустая нормальная форма эквивалентна И, в то время как нормальная форма, содержащая только пустой дизъюнкт, экви-валентна Л.
Дизъюнкт общезначим тогда и только тогда, когда он со-держит пару противоположных литер. Единственным невыпол-нимым дизъюнктом является пустой дизъюнкт Л.
Нормальная форма общезначима тогда и только тогда, ко-гда все ее дизъюнкты общезначимы.
В качестве примера приведем к КНФ формулу

Каждая из нижеприведенных формул эквивалентна исход-ной.
Первый этап (исключение импликации):

Второй этап (перенос и снятие отрицания):

Третий этап (применение дистрибутивности и упрощение):

Нормальная форма содержит единственный дизъюнкт . Отсюда следует, что исходная формула ложна только когда р и s истинны, а q и r ложны.
Двойственным понятием к дизъюнкту является произведе-ние, или конъюнкт, конечного множества литер. Дизъюнктивная нормальная форма (ДНФ) — дизъюнкция конечного числа конъюнктов. Можно показать, что любая формула приводится к логически эквивалентной ей ДНФ.

Принцип резолюций

Не существует общего, по-настоящему эффективного кри-терия для проверки выполнимости КНФ. Тем не менее есть дос-таточно удобный метод для выявления невыполнимости множе-ства дизъюнктов. Действительно, множество дизъюнктов невы-полнимо тогда и только тогда, когда пустой дизъюнкт Л являет-ся логическим следствием из него. Таким образом, невыполни-мость множества S можно проверить, порождая логические следствия из S до тех пор, пока не получим пустой дизъюнкт.
Для порождения логических следствий будет использоваться очень простая схема рассуждений. Пусть А, В и X — формулы. Предположим, что две формулы и — истин-ны. Если X тоже истинна, то отсюда можно заключить, что В истинна. Наоборот, если X ложна, то можно заключить, что А истинна. В обоих случаях истинна. Получается правило

которое можно записать также в виде

В том частном случае, когда X — высказывание, а А и В — дизъюнкты, это правило называется правилом резолюций. Об-щезначимость правила резолюций выражается следующей лем-мой.
Лемма 1. Пусть s1 и s2 — дизъюнкты нормальной формы S, l — литера. Если и , то дизъюнкт является логическим следствием нормальной формы S.
Следствие. Нормальные формы S и эквивалентны.
Замечание. Дизъюнкт r называется резольвентой дизъюнк-тов s1 и s2.

Доказательства невыполнимости, основанные
на принципе резолюций

Доказательства невыполнимости логических формул очень важны в искусственном интеллекте (ИИ). Способы таких дока-зательств, основанные на принципе резолюций, выделяются среди прочих тем, что они дают возможность использовать средства автоматического доказательства, применяемые в логи-ческом программировании.
При всей простоте метод резолюций (или, короче, резолю-ция) достаточен для обнаружения возможной невыполнимости множества приведенных дизъюнктов. Таким образом, можно попробовать доказать невыполнимость конечного множества дизъюнктов из S с помощью следующего алгоритма.
При условии, что Л ,
выбираем l, s1, s2, такие, что и ;
вычисляем резольвенту r;
заменяем S на .
В качестве примера проверим невыполнимость множе-ства
.
Дизъюнкты удобно пронумеровать. Получится следую-щий список:

Затем вычисляются и добавляются к S резольвенты. В спи-ске, который приводится ниже, каждый дизъюнкт — резольвен-та некоторых из предшествующих дизъюнктов. Номера их при-ведены в скобках справа от соответствующей резольвенты.
5. (1,3)
6. (1,4)
7. (2,3)
8. (2,4)
9. (2,5)
10. (3,6)
11. (3,8)
12. (4,5)
13. (4,7)
14. Л (4,9)
Замечание. Алгоритм проверки невыполнимости — неде-терминированный: вообще говоря, возможен не один выбор для l, s1 и s2. В приведенном примере мы выбирали дизъюнкты s1 и s2 в лексикографическом порядке номеров. Такая стратегия не-оптимальна. Некоторые резольвенты оказались ненужными, а также вычислялись в некоторых случаях более одного раза. Для сравнения продемонстрируем теперь применение этого же алго-ритма с минимумом резолюций:
5. (1,4)
6. (2,4)
7. (3,6)
8. Л (5,7)
Ясно, что принятая стратегия может значительно влиять на процесс выполнения алгоритма. Тем не менее упомянем два важных свойства, не зависящих от используемой стратегии.
Прежде всего, если множество S не содержит ни одной па-ры дизъюнктов, допускающих резольвенту, то оно выполнимо (разумеется, за исключением случая, когда оно содержит пустой дизъюнкт). Интерпретация I получается заданием I(p)= И тогда и только тогда, когда положительная литера р принадлежит од-ному из дизъюнктов множества S.
Во-вторых, если выполнение этого алгоритма закончилось «нормально» после порождения пустого дизъюнкта, то установ-лена невыполнимость исходного множества S. Это непосред-ственное следствие леммы 1.
Может случиться, что выполнение алгоритма не завершит-ся, хотя число различных дизъюнктов, которые могут быть по-рождены с помощью резолюций, очевидно, конечно.
Представляет интерес свойство завершаемости метода ре-золюций: конечное множество S невыполнимо тогда и только тогда, когда пустой дизъюнкт может быть выведен из S с помо-щью резолюций. Из леммы 1 следует достаточность этого усло-вия. Пустой дизъюнкт, будучи невыполнимым, не может быть логическим следствием из выполнимого множества дизъюнктов. Необходимость сформулированного условия отражена в сле-дующей лемме.
Лемма 2. Если множество дизъюнктов S невыполнимо и содержит резольвенты своих элементов, то оно обязательно со-держит пустой дизъюнкт.
Замечание. Ясно, что число различных дизъюнктов, кото-рые можно составить на основе конечного множества S, конеч-но. Таким образом, лемма 2 дает простое общее средство реше-ния вопроса о выполнимости или невыполнимости конечного множества дизъюнктов.
Лемма 1 остается справедливой для бесконечного S. Отсю-да следует, что бесконечное множество дизъюнктов невыпол-нимо тогда и только тогда, когда в нем найдется конечное невы-полнимое подмножество. Приведем непосредственное следст-вие, отражающее свойство завершаемости принципа резолюций.
Следствие 3. Если множество S формул невыполнимо, то этот факт всегда можно установить методом резолюций.

1.2 Исчисление предикатов

Словарь, синтаксис, семантика

Исчисление высказываний [8] позволяет формализовать лишь малую часть множества рассуждений. Например, рассмот-рим следующее рассуждение:
Все люди смертны;
Сократ — человек; (1.4)
следовательно, Сократ смертен.
Это рассуждение правильное, но оно выходит за рамки ло-гики высказываний. В нем содержатся три высказывания:
р : Все люди смертны,
q : Сократ — человек,
r : Сократ смертен.
Используя соответствующие связи, можно написать формулу

Эта формула не общезначима. Таким образом, логика вы-сказываний не позволяет корректно выразить рассуждение (1.4). Причина этой неудачи довольно очевидна. Логика высказыва-ний моделирует высказывания и функционально-истинностные связки, позволяющие комбинировать высказывания. В таком контексте высказывание — неделимый объект. Однако ясно, что в естественных языках высказывание имеет внутреннюю струк-туру. Иначе говоря, значение высказывания, хотя бы в первом приближении, является функцией значений его компонент.
До того как будет рассмотрен собственно семантический аспект, даже простой лексический анализ обнаруживает инте-ресное сходство между тремя высказываниями приведенного в примере рассуждения: некоторые слова присутствуют в этом рассуждении более одного раза. Следовательно, можно предпо-ложить, что указанное сходство должно сохраниться в формаль-ной версии этого рассуждения.
С другой стороны, в естественном языке часто опускают легко восполняемые слова. Текст (1.4) в этом отношении не ис-ключение. Мы уже заметили наличие связки конъюнкции, обо-значенной в тексте точкой с запятой. Первое высказывание со-держит также скрытую импликацию. Его можно переписать следующим образом:
Быть человеком — значит быть смертным.
Эта переформулировка не вполне удовлетворительна: такое впечатление, что ей соответствует формула типа . Это не так: слово «быть» устанавливает связь между посылкой А и следствием В условного наклонения. Впрочем, заметим, что слово «Сократ» устанавливает аналогичную связь между двумя последними строками в (1.4). Между тем эти случаи различны: слово «быть» означает какой-то, пока не определенный, член некоторого универсума, тогда как «Сократ» означает конкрет-ный член этого универсума. По аналогии с языком математики говорят, что «быть» — это переменная (заново обозначим ее, как это принято, через х), тогда как «Сократ» — константа.
Текст (1.4) можно переписать так, что будет лучше видна его реальная структура, а именно следующим образом.
Для всех х, если х является человеком,
то х является смертным; (1.5)
Сократ является человеком;
(следовательно) Сократ является смертным.
Теперь можно пополнить запас различных составляющих. В дополнение к высказываниям и связкам (неявной конъюнкции, импликации вида «если ..., .... то» и импликации вида «следова-тельно») у нас есть разные новые компоненты: «для всех», «х», «Сократ», «является человеком» и «является смертным».
Такие обороты речи служат примерами предикатных кон-стант. Предикатная константа не меняет своего значения ис-тинности. Она лишь связана с подходящим числом аргументов или параметров, называемых термами. Это число мест зависит только от рассматриваемой предикатной константы. Последняя вместе с подходящим числом термов называется предикатной формой.
Выражение «для всех х» служит примером квантификации, которая состоит из квантора (здесь «для всех») и одной пере-менной (здесь х). Естественные языки содержат не только ог-ромное число связок, но и громадное число кванторов. Заметим для начала, что отрицанием выражения
для всех х, А
очевидно будет
существует (хотя бы один) х,
Таким образом, нужен квантор «существует». Другие воз-можные кванторы:
Почти для всех...
Ровно для одного...
Существует ровно один...
Существует не более одного...
Существует много...
Существует бесконечно много...
Существует ровно пять...
Мы ограничимся квантором «для всех» и теми кванторами, которые можно из него получить с помощью пропозициональ-ных связок и, возможно, посредством отношения равенства, ко-торое будет введено далее. Уместно отметить, что в естествен-ном языке квантификация очень часто лишь подразумевается, но явно не представляется — например во фразах: «Все люди смертны», «Некоторые люди умерли».
Теперь мы можем формализовать гипотезы и заключение рассуждения (1.5). Квантор «для всех» обозначим , высказы-вание «с — человек» представим через Н(с), a «d смертен» за-пишем как M(d). Таким образом, получим полуформальное рас-суждение:
и H(Сократ), следовательно, М(Сократ)
По виду формул можно понять, что М и Н — одноместные предикатные константы, т.е. М и Н допускают единственный аргумент. Заметим также, что х — переменная (только одна пе-ременная может следовать за квантором). Напротив, ниоткуда не следует, что «Сократ» — константа.
Основными символами языка являются переменные, индивид-ные константы, предикатные константы, связки ( ), кванторы общности (для всех) и существования (сущест-вует). В языке предикатов содержится язык высказываний, так как высказывание — не что иное, как предикатная константа без аргументов или, точнее, предикатная константа с нулевым чис-лом мест. Удобно заменить понятие индивидной константы более общим понятием функциональной константы. Функциональная константа с определенным числом мест — в точности то же, что предикатная константа. Индивидная константа — просто нульме-стная функциональная константа.
Следующая лексика является обычной и будет полезна для понимания примеров, приводимых в этом разделе:
x, у, z переменные,
а, b, с индивидные константы,
f, g, h функциональные константы,
р, q, r высказывания,
Р, Q, R предикатные константы.
Словарь позволяет определить термы, формы и квалифи-кации (все они уже упоминались), а также атомы и формулы. Теперь изложим правила соответствующих построений.
• Термом является всякая переменная и всякая функцио-нальная форма.
• Функциональная форма — это функциональная кон-станта, соединенная с подходящим числом термов. Если f — функциональная n-местная константа и t1,..., tn — термы, то со-ответствующая форма обычно обозначается через f(t1,…, tn). Ес-ли п = 0, то пишут Р вместо Р( ).
• Предикатная форма — это предикатная константа, соединенная с подходящим числом термов. Если Р — предикат-ная m-местная константа и t1,..., tm — термы, то соответствующая форма обычно обозначается через P(t1,..., tm). При m=0 пи-шут Р вместо Р ( ).
• Атом — это предикатная форма или некоторое равен-ство, т.е. выражение типа (s = t), где s и t — термы.
• Понятие формулы определяется рекурсивно (ин-дуктивно) следующими правилами:
- атом есть формула;
- если А — формула, то А — формула;
- если А и В — формулы, то — формулы;
- если А — формула и х — переменная, то хА и хА — формулы.
Переменные в логике играют роль, аналогичную их роли в алгебре или анализе. Прежде всего они позволяют указать в структуре математического объекта те места, которые при ис-пользовании этого объекта будут заняты другими объектами. Например, линейная функция f может быть записана классиче-ской формулой
f(x)=x+6;
или еще с помощью обозначения, подчеркивающего статус объ-екта f, формулой типа
f= x.x+6.
В этом контексте х означает не объект, а место для объекта. Можно без хлопот переобозначить х, т.е. заменить два вхождения х, например, на у. Очевидно, что нельзя заменить только одно вхо-ждение, а другое оставить без изменения. Такой тип замены называется одновременной подстановкой. Говорят, что х — связанная переменная, желая тем самым отразить то обстоятельство, что пер-вое вхождение х вводит (описывает) связь, которой подчинено второе вхождение х. Переименование связанной переменной до-пустимо, так как сколько было различных вхождений переменных до одновременной подстановки, столько же останется и после.
Из интуитивного понимания квантификации вытекает, что имеется связь между вхождениями переменной, содержащейся в квантификации. В формуле

переменная х «связана». Связь вводится первым вхождением, которое следует непосредственно после квантора общности.
Область действия некоторой квантификации есть формула, к которой применяется эта квантификация. Вхождение пере-менной х, появляющейся в квантификациях или , называ-ется квалифицированным. Каждое вхождение переменной х в область действия этой квантификации является связанным. Вхождение переменной х свободное, если оно не является ни квантифицированным, ни связанным.
Замечания. Часто употребляют выражение «область дейст-вия квантора» вместо «область действия квантификации».
Переменная, имеющая связанное вхождение в некоторую формулу, имеет также квантифицированное вхождение в эту формулу.
В некоторой данной формуле переменная является кванти-фицированной (связанной, свободной), если она имеет хотя бы одно квантифицированное (связанное, свободное) вхождение.
В формулах xA и хА область действия х есть А. Если х и у — переменные, то области действия х и у либо не пересекают-ся, либо одна вложена в другую.
Рассмотрим следующие примеры:

В первом случае две квантификации по одной и той же пе-ременной перекрываются. Мы не желаем сопоставлять семанти-ку этому типу формул, его мы исключим из рассмотрения, под-чиняясь следующему правилу введения кванторов:
и — формулы только в том случае, если х — пере-менная и А — формула, не содержащая связанных вхождений х.
Во втором случае две связанные переменные случайно по-лучили одно и то же имя. Это совсем незначительное затрудне-ние.
В третьем случае и связанная, и свободная переменные по-лучили одно и то же имя. Хотя это допустимо, лучше переиме-новать связанную переменную и написать, например,

Формулы исчисления предикатов, как и формулы исчисления высказываний, могут быть интерпретированы, т.е. мо-гут получить значение истинности. Однако формулы исчисле-ния предикатов состоят не только из подформул, но также и из термов. Следовательно, необходимо будет интерпретировать также термы. Терм интуитивно означает объект. Таким обра-зом, интерпретация должна специфицировать множество объектов, называемое областью интерпретации.
Точнее, интерпретация I — это тройка (D, Ic, Jv) со сле-дующими свойствами:
• D — непустое множество, область интерпретации:
• IС — функция, которая сопоставляет каждой функцио-нальной n-местной константе f некоторую функцию IС(f) из Dn в D и которая сопоставляет каждой предикатной m-местной константе Р некоторую функцию IС(Р) из Dm в {И, Л};
• Iv — функция, сопоставляющая каждой переменной не-который элемент из D.
Теперь можно задать для интерпретации I = (D, Ic, Iv) такие правила, которые каждой формуле A ставят в соответствие не-которое значение истинности I(A), а каждому терму t сопостав-ляют элемент I(t) из D.
• Если х — свободная переменная, то I(х) =defIv(x).
• Если f — функциональная n-местная константа, t1 , ..., tn — термы, то I(f(t1,…,tn))=def=(Ic(f))(I(t1),…,I(tn)).
• Если Р — предикатная m-местная константа, t1, … , tm — термы, то I(P(t1,…,tm))=def=(Ic(P))(I(t1),…I(tm)).
• Если s и t — термы, то I(s=t) есть И при I(s)=I(t), а иначе Л.
• Если A и В — формулы, то ,

интерпретируются как в исчислении высказываний.
Осталось задать интерпретацию для двух типов квантифици-рованных формул. Введем сначала одно понятие. Если I — ин-терпретация с областью DI, х — переменная, d — элемент из DI, то Ix/d означает такую интерпретацию J, что DJ = DI, Jc = Ic, Jv(x)=d и Jv (y)= Iv(y) для всех свободных переменных у, отлич-ных от x.
Правила интерпретации будут такими:
• Если A — формула и х — переменная, то есть И при условии, что Ix/d(A) есть И для всех элементов d из D.
• Если А — формула и х — переменная, то есть И при условии, что 1х/d(А) есть И хотя бы для одного элемента d из D.
Формула А исчисления предикатов называется истинной при интерпретации I, если
I(A) = И.
Теперь видно, что запрещение перекрытия кванторов, дей-ствующих на одну и ту же переменную, не является существен-ным ограничением. В частности, интерпретируется как и интерпретируется как . Ясно также, почему требуется условие : без него естественные импликации

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


Подстановка и конкретизация

Подстановка есть отображение множества переменных V во множество термов Т. Подстановка конечна, если отлично от х лишь для конечного числа элементов из V. Подстановка а бу-дет задаваться множеством таких пар , что .
Пусть t — терм и  — подстановка. Терм [t] получается одновременной заменой всех вхождений переменной х в t на их образы относительно (х). Вот пример:
 = {(x, f(x)), (y, g(x,z))},
t = g(f(x), g(f(z), y)),
[t]= g(f(f(x)), g(f(z), g(x,z))).
Эта манипуляция сопоставляет каждой подстановке  неко-торую функцию из Т в Т, которая отображает t в [t]. Так как для всех переменных х имеем [х]= (х), то эта новая функция является продолжением . Обозначим ее тоже через .
Композиция двух подстановок 1 и 2 есть функция , определяемая следующим образом:

Если подстановки 1 и 2 таковы, что для любой перемен-ной х хотя бы один из термов 1(x),2(х) равен х, то объединение образов 1 и 2 определяет еще одну подстановку, которая на-зывается объединением подстановок 1 и 2 и обозначается че-рез .
Терм t2 называется конкретизацией (для) терма t1, если су-ществует подстановка , такая, что t2 = [t1]. Множество пере-менных терма t обозначим через var(t). Терм t вполне конкрети-зирован, если var(t)=.
Отношение «является конкретизацией (для)» обозначим символом .

Предваренная и нормальные формы

В логике высказываний были введены две нормальные формы: конъюнктивная и дизъюнктивная. Мы видели, что при-ведение формулы логики высказываний к одной из этих нор-мальных форм позволяет упростить алгоритмы доказательства выполнимости общезначимости. По аналогичным причинам стоит ввести нормальные формы и в исчисления предикатов.
Проблемы, возникающие при оперировании с квантифика-циями и областями действия кванторов, иногда бывают доста-точно сложными. В частности, к некоторым трудностям может привести одновременное присутствие в формуле свободных и связанных вхождений одной и той же переменной. Положение заведомо проще для случая предваренных форм.
Предваренной формой называется формула, состоящая из матрицы, перед которой стоит префикс, т.е. некоторая конечная последовательность квантификаций. Эти квантификации отно-сятся к различным переменным, и их порядок вообще является существенным. Таким образом, формула имеет вид
Q1x1 … QnxnM,
где символ Qi означает либо , либо , для i = l, ..., п и где М — формула (матрица), не содержащая квантификации.
Без ограничения общности можно потребовать, чтобы кван-тифицированы могли быть только переменные, имеющие вхож-дение (обязательно свободное) в матрицу. Действительно, по правилам интерпретации, если формула А не содержит вхожде-ний переменной х, то формулы и имеют одно и то же значение истинности при всех интерпретациях.
Теорема 1.2. Для любой логической формулы существует логически эквивалентная ей предваренная форма.
Доказательство. Алгоритм получения предваренной фор-мы очень прост. Этапы таковы:
• Исключить связки эквивалентности и импликации по правилам преобразования.
• Переименовать (если необходимо) связанные перемен-ные таким образом, чтобы никакая переменная не имела бы од-новременно свободных и связанных вхождений. Это условие требуется не только для рассматриваемой формулы, но также для всех ее подформул.
• Удалить те квантификации, область действия которых не содержит вхождений квантифицированной переменной. Та-кие квантификации в действительности не нужны.
• Преобразовать все вхождения отрицания в стоящие не-посредственно перед атомами в соответствии со следующими правилами:

• Переместить все квантифнкации в начало формулы. Для этого используется соответствующий набор правил преобразо-вания. Здесь мы приведем эти правила для конъюнкции. Парные им правила для дизъюнкции получаются применением двойст-венности.

если В не содержит х,
если А не содержит х,
если В не содержит х,
если А не содержит х.
Для полноты этого набора правил необходимо добавить возможность переименования некоторых связанных перемен-ных. Например, формула будет сначала преоб-разована в (перед применением правил преоб-разования). Итак, теорема конструктивно доказана.
В качестве приложения найдем предваренную форму, экви-валентную формуле

Этапы этого поиска последовательно перечислены ниже.
Исключение связки импликации:

Переименование:

Удаление бесполезной квантификации:

Применение правил, касающихся отрицания:

Перемещение квантификации:

Замечание. Одна формула может допускать много эквива-лентных предваренных форм. Вид полученного результата зави-сит от порядка применения правил, а также от произвола при переименовании.
Понятия литеры, дизъюнкта и КНФ, введенные в исчислении высказываний, непосредственно распространяются на исчисление предикатов. Литера — это атом или его отрицание, дизъюнкт — дизъюнкция литер, конъюнктивная нормальная форма — предваренная форма, матрица которой есть конъюнк-ция дизъюнктов. Равным образом можно использовать двойст-венные понятия: импликант (конъюнкт) есть конъюнкция ли-тер, дизъюнктивная нормальная форма — это предваренная форма, матрица которой есть дизъюнкция импликантов.

Сколемовские и клаузальные формы

Механизм квантификации, очевидно, не только основа мо-гущества, но и источник сложности исчисления предикатов. Предваренные и нормальные формы особенно интересны тем, что, с одной стороны, они требуют лишь «дисциплинированно-го» использования квантификации, и с другой стороны, они со-храняют всю выразительную силу исчисления предикатов. Дей-ствительно, любая формула допускает эквивалентную нормаль-ную форму (хотя иногда более громоздкую или менее обозри-мую, чем исходная формула).
Можно установить еще более строгие пределы исполь-зования механизма квантификации ценой приемлемого умень-шения выразительной мощи. Точнее, будет предложено средст-во сопоставления каждой формуле А некоторой формулы SA очень простого строения с гарантией, что формулы А и SA либо обе выполнимы, либо обе невыполнимы. Эта связь между А и SA строго слабее, чем логическая эквивалентность, но все-таки она очень полезна по следующей причине. Предположим, что мы хотим доказать, что заключение С является логическим следст-вием гипотез Н1 и Н2. Это сводится к доказательству невыпол-нимости формулы G: , или же невыполнимости соответствующей формулы SG.
Без ограничения общности можно рассматривать только предваренные формы, потому что любая формула допускает эк-вивалентную предваренную форму. Кроме того, достаточно оперировать с замкнутыми формулами, т.е. без свободных пе-ременных. Действительно, если А — формула со свободными переменными х1, ..., хп, которая не содержит ни одного связанного вхождения переменных х1, ..., хп (после осуществления пе-реименования), то формула , с одной стороны, замк-нута и, с другой стороны, выполнима тогда и только тогда, ко-гда выполнима формула А.
Форма SA, которую мы сейчас опишем, известна под назва-нием сколемовской формы (соответствующей формуле А). Све-дение А к SA представляет особый интерес, потому что доказа-тельство невыполнимости становится эффективнее, если огра-ничиться только формулами, представленными в сколемовской форме. Приведение произвольной формулы исчисления преди-катов к сколемовской форме требует двух предварительных операций:
• Привести данную формулу к предваренной форме, со-стоящей из префикса и матрицы.
• Привести затем матрицу к КНФ.
Результатом будет замкнутая предваренная форма. Сколе-мовская форма, соответствующая ей (и, следовательно, исход-ной формуле), получится применением следующей процедуры, называемой сколемовским преобразованием и служащей для исключения -квантификаций.
• Сопоставить каждой -квантифицированной перемен-ной список -квантифицированных переменных, предшест-вующих ей, а также некоторую ещё не использованную функ-циональную константу, число мест у которой равно мощности списка.
• В матрице нашей формулы заменить каждое вхождение каждой -квантифицированной переменной на некоторый терм. Этот терм является функциональной константой, соответствующей данной переменной и снабженной списком аргументов, также соответствующим той же самой переменной.
• Устранить из формулы все -квантификации.
Обратимся вновь к примеру из предыдущего параграфа. Преобразуем формулу
.
Осуществленные в предыдущем параграфе преобразования привели нас к следующей КНФ:
.
Описанная выше процедура позволяет получить сколемов-скую форму, соответствующую исходной формуле:
.
Рассмотрим более пристально связь между формулой и ее формой Сколема. Например, обратимся к замкнутой предварен-ной форме
А : .
Ей соответствует сколемовская форма
SA : .
Предполагается, что функциональные константы а, f и g не входят в матрицу М(и, v, w, х, y, z).
Констатируем сразу же, что формула ( ) общезначи-ма. Отсюда следует, что если формула А невыполнима, то фор-мула SA тоже невыполнима. Наоборот, предположим, что фор-мула А выполнима и принимает истинное значение при некото-рой интерпретации I в области D. Положим М = IС(М). Для лю-бых V, X, Y существуют элементы A, В, С D, такие, что М(A, V, В, X, Y, С) истинно в D. Обратив внимание на относительное положение кванторов в формуле А, видим, что A не зависит от V, X и Y, что В может зависеть от V (но не от X и Y), что, наконец, С может зависеть от V, X и Y. Для получения интерпрета-ции, при которой истинна формула SA, достаточно интерпрети-ровать f и g как подходящие функции выбора F и G, т.е. такие, что F(V) и С(V, X, Y) были бы допустимыми значениями В и С.
Отметим, что сколемовская форма есть предваренная фор-ма, префикс которой содержит только -квантификации. С другой стороны, каждая предваренная форма такого специаль-ного типа является ее собственной сколемовской формой. По-этому удобно соединить эти два понятия. Когда позволяет кон-текст и особенно когда типографические условности дают воз-можность отличать индивидные константы от переменных, пре-фикс сколемовской формы можно опустить: подразумевается, что каждая присутствующая в матрице переменная -кван-тифицирована. В этом случае, пожалуй, лучше говорить о кон-кретизации для сколемовской формы, а не о конкретизации для матрицы сколемовской формы.
Клаузальной формой называется такая сколемовская форма, матрица которой является КНФ. Любая сколемовская форма допускает эквивалентную клаузальную форму.

Унификация

Так как дизъюнкт может допускать бесконечно много кон-кретизаций, то фундаментальный метод резолюций непременно неэффективен. Идея Робинсона состоит в том, чтобы работать прямо с самими дизъюнктами без явного рассмотрения их фун-даментальной конкретизации. Эта идея требует использования операции унификации. Прежде чем объяснить, о чем идет речь, отметим, что унификация — это основной механизм при выполнении инструкций в логическом программировании.
Пусть два дизъюнкта
C1 = {l1, ...} и C2 = { l2, …}
принадлежат множеству S. Посредством переименования можно исключить одновременное появление одной и той же перемен-ной в С1 и C2. Предположим, что литеры l1 и l2 являются унифи-цируемыми, т.е. они обладают общей фундаментальной конкре-тизацией. Из каждой пары фундаментальной конкретизации
и ,
таких, что , получается резольвента

Каждый дизъюнкт такого типа является логическим следст-вием из С1 и С2. Задача состоит в том, чтобы найти такой дизъ-юнкт R, фундаментальные конкретизации которого были бы в точности конкретизациями того типа, как для R`. Этот дизъюнкт R «представлял бы» подходящим образом множество таких кон-кретизаций. Обозначим через lи наибольшую нижнюю грань па-ры {l1, l2} относительно порядка . Имеем l` l1 и l` l2, что эквивалентно l` lu. По определению lи существуют подстановки и , такие что и . Так как ни-какая переменная не появляется одновременно в l1 и l2, то имеем также для .Подстановка явля-ется наиболее общим унификатором (НОУ) литер l1 и l2 (это обозначение не приводит к единственности ).
Резольвентным дизъюнктом R с требуемым свойством будет
.
Два атома унифицируемы, если они построены из одной предикатной константы, примененной к попарно унифицируе-мым термам. Таким образом, достаточно рассмотреть унифика-цию двух термов. Если один из них — переменная, то унифика-ция получается мгновенно. В противном случае для унифици-руемости два терма должны быть построены из одной и той же функциональной константы, примененной к попарно унифици-руемым термам.
Очевидно, получается (рекурсивный) алгоритм унификации — очень простой и линейной сложности относительно числа тер-мов. Все-таки следует указать на одну трудность. В частном случае, когда один из термов есть переменная х, а другой со-держит х, но не сводится к х, унификация, конечно же, невоз-можна. Систематическая проверка невхождения некоторой пе-ременной в терм, подлежащий унификации с этой переменной, приводит к неэффективному алгоритму. Тем не менее, можно в некоторой мере найти средство для решения этой проблемы. Проверку невхождения часто опускают в логическом програм-мировании.

Метод резолюций

С помощью унификации можно легко распространить алго-ритм резолюций на исчисление предикатов. Пусть S — множе-ство дизъюнктов, исследуемое на невыполнимость. Алгоритм таков:
Пока
искать такие, что
s1 и s2 есть дизъюнкты или факторы дизъюнктов;
унифицируемы, вычислить резоль-вентный дизъюнкт r, заменить S на S{r}.
Преобразованный таким способом метод резолюций полно-стью остается в силе.
Замечание. Напомним, что все переменные, входящие в дизъюнкт, связанные и их можно переименовывать.
Для примера применим метод резолюций к доказательству того, что если G — группа, каждый элемент которой является обратным самому себе, то G коммутативна. Гипотезы и заклю-чение такие:

Для исключения предиката равенства, не введенного в на-шем изложении данного метода, полагаем

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







Первые два дизъюнкта означают ассоциативность. Точнее, первый гласит, что можно переписать как , то-гда как второй — что можно переписать как . Отметим также, что отношение эквивалентно форму-ле , сколемовская форма которой есть .
Пустой дизъюнкт Л можно получить так, как показано ни-же. (В правой части списка указаны номера дизъюнктов, над которыми осуществляется резолюция, а также используемые унификаторы).
8.
1{(y,x),(u,e)}, 5.
9.
2{(x,a),(y,b),(u,c)},6.
10.
4{(x,z)}, 8{(w,z)}.
11.
5{(x,b)}, 9{(z,b),(v,e)}.
12.
3{(x,a)}, 11{(w,a)}.
13.
10{(x,c),(z,b),(v,a)}, 12.
14.
2{(v,e),(z,y)}, 5{(x,y)}.
15.
3, 14{(w,x)}.
16.
13, 15{(x,c),(y,a),(u,b)}.
17. Л 7, 16.

Правило согласия двойственно правилу резолюций. Если литеры l1 и l2 допускают НОУ , то согласием конъюнкций и является конъюнкция .

1.3 Логическое представление

Представление — это действие, делающее некоторое поня-тие воспринимаемым посредством фигуры, записи, языка или формализма. Теория знаний изучает связи между субъектом (изучающим) и объектом. Знание (в объективном смысле) — то, что известно (то, что знаем после изучения).
Представление знаний — формализация истинных убежде-ний посредством фигур, записей или языков. Нас особенно ин-тересуют формализации, воспринимаемые (распознаваемые) ЭВМ. Возникает вопрос о представлении знаний в памяти ЭВМ, т.е. о создании языков и формализмов представления знаний. Они преобразуют наглядное представление (созданное посред-ством речи, изображением, естественным языком, вроде фран-цузского или английского, формальным языком, вроде алгебры или логики, рассуждениями и т.д.) в пригодное для ввода и об-работки в ЭВМ. Результат формализации должен быть множеством инструкций, составляющих часть языка программи-рования.
Представлению знаний присущ пассивный аспект: книга, таблица, заполненная информацией память. В ИИ подчеркива-ется активный аспект представления: знать должно стать ак-тивной операцией, позволяющей не только запоминать, но и из-влекать воспринятые (приобретенные, усвоенные) знания для рассуждений на их основе. Следовательно, истоки представле-ния знаний — в науке о познании, а его конечная цель — про-граммные средства информатики.
Во многих случаях подлежащие представлению знания от-носятся к довольно ограниченной области, например:
• описание состояния Морфлота,
• описание ситуаций в игре (например, расположения фи-гур в шахматах),
• описание размещения персонала предприятия,
• описание пейзажа.
Для характеристики некой области говорят об «области рассуждений» или «области экспертизы». Численная формали-зация таких описаний в общем малоэффективна. Напротив, ис-пользование символического языка, такого как язык математи-ческой логики, позволяет формулировать описания в форме, од-новременно близкой и к обычному языку, и к языку программи-рования. Впрочем, математическая логика позволяет рассуж-дать, базируясь на приобретенных знаниях: логические выводы действительно являются активными операциями получения но-вых знаний из усвоенных.

Синтаксис логики предикатов

Язык логики предикатов задается синтаксисом. Для пред-ставления знаний базисные синтаксические категории языка изображаются такими символами, которые несут достаточно четкую информацию и дают довольно ясную картину об облас-ти рассуждений (экспертизы).
Логика предикатов, называемая также логикой первого по-рядка, допускает четыре типа выражений:
• Константы. Они служат именами индивидуумов (в от-личие от имен совокупностей): объектов, людей или событий. Константы представляются символами вроде Жак_2 (добавле-ние 2 к слову Жак указывает на вполне определенного человека среди людей с таким именем), Книга_22, Посылка_8.
• Переменные. Обозначают имена совокупностей, таких как человек, книга, посылка, событие. Символ Книга_22 пред-ставляет вполне определенный экземпляр, а символ книга ука-зывает либо множество «всех книг», либо «понятие книги». Символами х, у, z представлены имена совокупностей (опреде-ленных множеств или понятий).
• Предикатные имена. Они задают правила соединения констант и переменных, например, правила грамматики, проце-дуры, математические операции. Для предикатных имен используются символы наподобие следующих: Фраза, Посылать, Пи-сать, Плюс, Разделить. Предикатное имя иначе называется предикатной константой.
• Функциональные имена представляют такие же правила, как и предикаты. Чтобы не спутать с предикатными именами, функциональные имена пишут одними строчными буквами: фраза, посылать, писать, плюс, разделить. Их называют также функциональными константами.
Символы, которые применяются для представления кон-стант, переменных, предикатов и функций, не являются «слова-ми русского языка». Они суть символы некоторого представле-ния — слова «объектного языка» (в нашем случае «языка пре-дикатов»).
Представление должно исключать всякую двусмысленность языка. Поэтому имена индивидуумов содержат цифры, припи-сываемые к именам совокупностей. Жак_1 и Жак_2 представ-ляют двух людей с одинаковыми именами. Эти представления суть конкретизации имени совокупности «Жак». Предикат — это предикатное имя вместе с подходящим числом термов. Пре-дикат называют также предикатной формой.

Примеры
Проиллюстрируем синтаксис логики предикатов, сопостав-ляя нескольким русским фразам их переводы на язык логиче-ского формализма.
• По-русски: Жак посылает книгу Мари,
Логически: Посылка (Жак_2, Мари_4, Книга_22).
• По-русски: Каждый человек прогуливается,
Логически: (Человек(х) Прогуливается(х)).
• По-русски: Некоторые люди прогуливаются,
Логически: (Человек(х) Прогуливается(х)).
(Сравнивая два последних примера, видим, что замена при-лагательного «каждый» на «некоторые» влечет при переводе не только замену квантора на , но и замену связки на . Это иллюстрирует тот факт, что перевод фразы естественного языка на логический, вообще говоря, не является трафаретной операцией.)
• По-русски: Ни один человек не прогуливается,
Логически: ( (Человек(х) Прогуливается(Х))).

Преобразование унарных предикатов в бинарные

Унарные и бинарные предикаты имеют соответственно один и два аргумента. Фраза «Сократ есть человек» представима унарным предикатом Человек(Сократ), а «Жак любит Мари» — бинарным Любит(Жак_2, Мари_4). Бинарные предикаты игра-ют особую роль в представлении знаний.
Любой унарный предикат можно преобразовать в бинарный следующим образом. Унарный предикат состоит из предикатно-го имени и значения своего единственного аргумента. Следова-тельно, его формат такой: Предикатное_имя (значение_ар-гумента). Значение аргумента есть конкретизация предикатного имени или переменной. Например, Человек(Сократ) указывает, что имя собственное «Сократ» — конкретизация имени сово-купности «человек», а Человек(х) указывает, что х — человек (не что-либо иное). Точно так же Женщина(Мари_4) означает, что «Мари» — «женщина». Введем бинарный предикат Конкр(значение_1, значение_2) и придадим ему следующий смысл: значение первого аргумента — имя индивидуума или элемент вполне определенного типа, значение второго аргумен-та — имя совокупности этого типа. Фразу «Сократ — человек» можно представить бинарным предикатом Конкр(Сократ, чело-век).
Таким образом, введенный бинарный предикат эквивален-тен исходному унарному в том смысле, что они оба представ-ляют одну и ту же фразу. Преобразование следующее:
Унарный предикат Бинарный предикат,
Имя совокупности Конкр(имя_индивиду-
(имя_индивидуума) ума, имя совокупности).
Таким образом, предикатное имя Конкр означает: «является элементом некоторого типа». Иногда этот предикат обозначают так: Есть_некий.

Примеры
Преобразуем унарные предикаты из примеров в эквива-лентные бинарные. Во втором примере имеются несколько эк-вивалентных версий.
• По-русски: Каждый человек прогуливается,
Логически: (Конкр(х, человек) Конкр(х, прогулива-ется)).
• По-русски: Ни один человек не прогуливается,
Логически-1: ( (Конкр(х, человек) Конкр(х, прогули-вается))),
Логически-2 ( (Конкр(х, человек) Конкр(у, прогу-ливается) Субъект(у, х))),
Логически-3: ( Конкр(х, человек) Конкр(y, про-гуливается) Субъект(у, х)).
Предикат Субъект (у, х) означает: переменная х есть субъ-ект события у; в данном случае «человек» — субъект события «прогуливается». Три логических представления эквивалентны. Они представляют синонимы одного и того же утверждения: «Неправда, что существует прогуливающийся человек»; «Неправда, что существуют х и у, где х — человек, у — прогулива-ется и x — субъект события у», «Для всех х и всех у либо х не человек, либо у не означает прогуливаться, либо же х не субъект события у».

Преобразование m-арных предикатов в произведение
бинарных

Фразу «Жак посылает книгу Мари» нетрудно представить тернарным (т.е. с тремя аргументами) предикатом:
Посылка (Жак_2, Мари_4, Книга_22).
Определив новые предикаты, можно представить эту фразу произведением (конъюнкцией) бинарных предикатов:
Отправитель (Посылка, Жак_2)
Получатель (Посылка, Мари_4)
Объект (Посылка, Книга_22).
Данная логическая формула читается так: «отправитель по-сылки — Жак, получатель посылки — Мари и объект посылки — книга».
Этот пример подсказывает правило преобразования m-арных предикатов (с m аргументами) в эквивалентное произве-дение бинарных предикатов. Всякий m-арный предикат состоит из предикатного имени и m значений аргументов:
Предикатное_имя(значение_1, значение_2, ..., значение_m).
В таких обозначениях подразумеваемые предикатом функ-циональные отношения выражены порядком аргументов. На-пример, предикат для описания посылки некоторого объекта отправителем получателю может иметь следующий формат:
Посылка (отправитель, получатель, объект).
Функция «отправитель посылки» учитывается первым ар-гументом, функция «получатель посылки» — вторым, функция «объект посылки» — третьим. Первоначально выбранный поря-док аргументов для соответствия «функция — аргумент» может быть произвольным, но должен сохраняться неизменным. Функциональную организацию m-арного предиката можно предста-вить так:
Предикатное_имя(функция_1, функция_2, ..., функция_т).
При записи m-арного предиката через бинарные предикаты используется специальное соглашение, позволяющее сохранить и явно указать соответствующие функциональные отношения. Каждая функция становится именем бинарного предиката, пер-вый аргумент которого является именем исходного m-арного предиката, а второй — значением относящегося к этой функции аргумента. Функциональная организация исходного m-арного предиката и значения его аргументов представляются произве-дением бинарных предикатов:
Функция_1(предикатное_имя, значение_1) Функция_m (предикатное_имя, значение_m).
Таким образом, имеем следующее преобразование:
Предикатное_имя(значение_1, …, значение_m) Функ-ция_j(предикатное_имя, значение_j).
Запись в терминах бинарных предикатов содержит в явном виде имена функциональных отношений, которые могли бы быть неявно представлены порядком следования аргументов при запи-си в терминах т-арных предикатов. Пара (функция_j, значение_j) называется слотом (по-английски slot). Слот состоит из своих имени (которое именует функциональное отношение) и ключа (который представляет значение функционального отношения, то есть значение j-го аргумента исходного m-арного предиката). Со-ответствующие английские термины slot, slot-name, slot-value; бинарный предикат вида Функция-j(предикатное_ имя, значе-ние_j) называется slot-assertion notation.

Явное представление ссылок

При представлении знаний в логической форме важно ис-ключить двусмысленности, которые вообще имеются в любом неформализованном представлении. Именно поэтому мы дали имена каждому индивидууму, появляющемуся в логической формуле. Символы объектного языка, такие как Жак_2, Мари_4 и Книга_22, введены для того, чтобы избежать двусмысленности ссылок на вполне определенных людей и книгу. Впрочем, мож-но постулировать, что фраза «Жак посылает книгу Мари» ука-зывает определенное «почтовое событие» (или «действие от-правления»), на которое желательно иметь возможность ссы-латься в дальнейшем. Следовательно, придется дать ему имя индивидуума Посылка_8 и указать, что оно — часть множества событий с именем совокупности посылки. Перевод фразы на бинарные предикаты выглядит так:
Отправитель(Посылка_8, Жак_2)
Получатель (Посылка_8, Мари_4)
Объект (Посылка_8, Книга_22)
Элем(Посылка_8, посылки)
Предикатное имя Элем означает «есть элемент такого-то множества»