№05 Алгоритмы унификации. Принцип резолюции (1006466)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

5. Алгоритмы унификации. Принцип резолюции

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

Описываемый ниже алгоритм предназначен для ответа на вопрос: "Как применить теорему к выражению?" Этот алгоритм не зависит от формальной системы, в которой применяется. Для заданных теоремы и выражения алгоритм выполняет в строгой последовательности двойной проход в предварительно определенном порядке. Его сложность линейно зависит от общего числа замещаемых переменных в теореме и выражении. В неявном виде этот алгоритм используется при некоторых доказательствах в различных формальных системах. Данный алгоритм, разработанный в 1966 г. Ж. Питра и не зависимо от него Дж. Робинсоном, играет фундаментальную роль в искусственном интеллекте.

Д ля данной теоремы Т в форме правила переписывания или продукции с антецедентом вида
H C (T)
(гипотеза) влечет (заключение)

и некоторого выражения Е необходимо проверить, можно ли сделать H и Е полностью идентичными, т. е. унифицировать H и E путем последовательных подстановок свободных переменных в H и Е. Подстановки, выполненные в С, дают новую форму выражения Е в результате применения теоремы Т (с использованием правила модус поненс).

Modus pones: Если есть формула А и есть формула А->В, то выводится В. А является антицидентом импликации А->В.

Пример унификации:. Пусть алгебраическое тождество
(а + b)² = a² + 2ab + b² (I1)
рассматривается в качестве удобного сокращенного представления правила переписывания: "Если какое-то выражение является квадратом суммы .двух термов, его можно переписать в виде суммы квадрата первого терма, удвоенного произведения обоих термов и квадрата второго терма". Пусть, кроме того, имеется выражение
x² + (y + √3) ² (E1)
В данном случае легко увидеть совпадение выражений в скобках в (I1) и (E1): подстановка у вместо а и √3 вместо b позволяет унифицировать (y + √3) и левый член тождества (I1).

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

Во всяком выражении только свободные переменные являются замещаемыми, т. е. те переменные, которые не являются квантифицированными (на них не распространяется действие кванторов всеобщности или существования). Единственно разрешенными подстановками являются такие, которые замещают свободную переменную х из Е или H термом t из Е или Н. Имеется только одно ограничение: терм t сам не должен уже содержать переменную х. Поэтому, чтобы избежать всякой неоднозначности и неопределенности, в первую очередь проводится "разделение имен" переменных из Е или T, каковы бы ни были их начальные имена.

Подстановки выполняются только по необходимости. Символы, которые не являются переменными, не могут замещаться. К таким символам относятся либо операторы (например, +, *, ->, sin...), либо константы (например, 1, 2, ...). Естественно, такие символы должны находиться на аналогичных позициях в Е и H, иначе невозможна никакия унификация.

Фундаментальная идея, лежащая в основе алгоритма, связана с процедурой просмотра выражения: вначале основной оператор, затем каждый из подтермов, которыми он управляет, начиная, например, с самого левого. Каждый подтерм при этом просматривается параллельно; основной оператор, подтерм и так далее до переменной или константы. Удобным для этого является представление выражения в виде дерева (рис. 1).

Рис. 1. Представление выражения
х² + (х + √З)²
и порядок его просмотра в соответствии с алгоритмом унификации.

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

Используя этот порядок просмотра (вначале вглубь), для задания последовательности просмотра введем индексы е и h: e — индекс текущего символа в выражении E и h — индекс текущего символа в выражении H.

В общем случае принцип рекуррентности формулируется следующим образом: пусть все символы в выражениях Е и Н совпадают вплоть до символов с индексами е и h, не включая их; попытаемся привести к совпадению символы с индексами е и h соответственно в Е и H.

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

Известно, что в начале процесса число переменных, замещаемых в выражениях Е и H, является конечным. С одной стороны, во время выполнения процедуры не создается новых переменных, а с другой, каждая подстановка, которая замещает переменную термом, не содержащим ее, приводит к уменьшению общего числа обрабатываемых переменных. Следовательно, алгоритм унификации является сходящимся при числе подстановок, большем или равном первоначальному числу свободных переменных в E и H.

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

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

В исчислении предикатов имеется множество правил вывода. В качестве примера приведем классическое правило отделения, или modus ponens :

(A, A B) / B

которое читается так "если истинна формула A и истинно, что из A следует B, то истинна и формула B". Формулы, находящиеся над чертой, называются посылками вывода, а под чертой - заключением. Это правило вывода формализует основной закон дедуктивных систем: из истинных посылок всегда следуют истинные заключения. Аксиомы и правила вывода исчисления предикатов первого порядка задают основу формальной дедуктивной системы, в которой происходит формализация схемы рассуждений в логическом программировании. Можно упомянуть и другое правило вывода.

Modus tollendo tollens : Если из A следует B и B ложно, то и A ложно.

Решаемая задача представляется в виде утверждений (аксиом) f₁, F₂... F_n исчисления предикатов первого порядка. Цель задачи B также записывается в виде утверждения, справедливость которого следует установить или опровергнуть на основании аксиом и правил вывода формальной системы. Тогда решение задачи (достижение цели задачи) сводится к выяснению логического следования (выводимости) целевой формулы B из заданного множества формул (аксиом) f₁, F₂... F_n. Такое выяснение равносильно доказательству общезначимости (тождественно-истинности) формулы

f₁& F₂&... & F_n B

или невыполнимости (тождественно-ложности) формулы

f₁& F₂&... & F_n& ¬B

Из практических соображений удобнее использовать доказательство от противного, то есть доказывать невыполнимость формулы. На доказательстве от противного основано и ведущее правило вывода, используемое в логическом программировании, - принцип резолюции. Робинсон открыл более сильное правило вывода, чем modus ponens, которое он назвал принципом резолюции (или правилом резолюции ). При использовании принципа резолюции формулы исчисления предикатов с помощью несложных преобразований приводятся к так называемой дизъюнктивной форме, то есть представляются в виде набора дизъюнктов. При этом под дизъюнктом понимается дизъюнкция литералов, каждый из которых является либо предикатом, либо отрицанием предиката.

Приведем пример дизъюнкта:

x (P(x, c₁) Q(x, c₂)).

Пусть P - предикат уважать, c₁ - Ключевский, Q - предикат знать,c₂ - история. Теперь данный дизъюнкт отражает факт "каждый, кто знает историю, уважает Ключевского".

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

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

Главная идея этого правила вывода заключается в проверке того, содержит ли множество дизъюнктов R пустой (ложный) дизъюнкт. Обычно резолюция применяется с прямым или обратным методом рассуждения. Прямой метод из посылок A, A B выводит заключение B (правило modus ponens). Основной недостаток прямого метода состоит в его не направленности: повторное применение метода приводит к резкому росту промежуточных заключений, не связанных с целевым заключением. Обратный вывод является направленным: из желаемого заключения B и тех же посылок он выводит новое подцелевое заключение A. Каждый шаг вывода в этом случае связан всегда с первоначально поставленной целью. Существенный недостаток метода резолюции заключается в формировании на каждом шаге вывода множества резольвент - новых дизъюнктов, большинство из которых оказывается лишними.

Процесс доказательства методом резолюции (от обратного) состоит из следующих этапов:

1. Предложения или аксиомы приводятся к дизъюнктивной нормальной форме.

2. К набору аксиом добавляется отрицание доказываемого утверждения в дизъюнктивной форме.

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

4. Генерируется пустое выражение, означающее противоречие.

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

Характеристики

Тип файла документ

Документы такого типа открываются такими программами, как Microsoft Office Word на компьютерах Windows, Apple Pages на компьютерах Mac, Open Office - бесплатная альтернатива на различных платформах, в том числе Linux. Наиболее простым и современным решением будут Google документы, так как открываются онлайн без скачивания прямо в браузере на любой платформе. Существуют российские качественные аналоги, например от Яндекса.

Будьте внимательны на мобильных устройствах, так как там используются упрощённый функционал даже в официальном приложении от Microsoft, поэтому для просмотра скачивайте PDF-версию. А если нужно редактировать файл, то используйте оригинальный файл.

Файлы такого типа обычно разбиты на страницы, а текст может быть форматированным (жирный, курсив, выбор шрифта, таблицы и т.п.), а также в него можно добавлять изображения. Формат идеально подходит для рефератов, докладов и РПЗ курсовых проектов, которые необходимо распечатать. Кстати перед печатью также сохраняйте файл в PDF, так как принтер может начудить со шрифтами.

Список файлов ответов (шпаргалок)