Методы поиска решений на основе исчисления предикатов


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

В исчислении высказываний основным объектом является переменное высказывание (предикат), истинность или ложность которого зависит от значений входящих в него переменных. Так, истинность предиката " x был физиком" зависит от значения переменной x. Если x - П. Капица, то предикат истинен, если x - М. Лермонтов, то он ложен. На языке исчисления предикатов утверждение читается так: "для любого x если P(x), то имеет место и Q(x) ". Иногда его записывают и так: . Выделенное подмножество тождественно истинных формул (или правильно построенных формул - ППФ), истинность которых не зависит от истинности входящих в них высказываний, называется аксиомами.

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

(A, A -> B) / B

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

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

Modus ponendo tollens : Если A и B не могут одновременно быть истинными и A истинно, то B ложно.

Modus tollendo ponens : Если либо A, либо B является истинным и A не истинно, то B истинно.

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

f1& F2&... & Fn -> B

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

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

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

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

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

Пусть P - предикат знать, c1 - физика, c2 - история. Данный дизъюнкт отражает запрос "кто знает физику и историю одновременно".

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

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

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

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

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

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

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

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

Рассмотрим примеры применения методов поиска решений на основе исчисления предикатов. Пример "интересная жизнь" заимствован из [ 1.1 ] . Итак, заданы утверждения 1-4 в левом столбце таблица 3.2 Требуется ответить на вопрос: "Существует ли человек, живущий интересной жизнью?" В виде предикатов эти утверждения записаны во втором столбце таблицы. Предполагается, что . В третьем столбце таблицы записаны дизъюнкты.

Таблица 3.2. Интересная жизнь
Утверждения и заключение Предикаты Предложения(дизъюнкты)
1. Все небедные и умные люди счастливы
2. Человек, читающий книги, - неглуп
3. Джон умеет читать и является состоятельным человеком
4. Счастливые люди живут интересной жизнью
5. Заключение: Существует ли человек, живущий интересной жизнью? exciting(W)
6. Отрицание заключения

Отрицание заключения имеет вид (строка 6):

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

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

2. резольвента 7 и 1

3. резольвента 8 и 2

4. резольвента 9 и 3b

5. NIL резольвента 10 и 3a

Символ NIL означает, что база данных выражений содержит противоречие и поэтому наше предположение, что не существует человек, живущий интересной жизнью, неверно.

В методе резолюции порядок комбинации дизъюнктивных выражений не устанавливался. Значит, для больших задач будет наблюдаться экспоненциальный рост числа возможных комбинаций. Поэтому в процедурах резолюции большое значение имеют также эвристики поиска и различные стратегии. Одна из самых простых и понятных стратегий - стратегия предпочтения единичного выражения, которая гарантирует, что резольвента будет меньше, чем наибольшее родительское выражение. Ведь в итоге мы должны получить выражение, не содержащее литералов вообще.

Среди других стратегий (поиск в ширину (breadth-first), стратегия "множества поддержки", стратегия линейной входной формы) стратегия "множества поддержки" показывает отличные результаты при поиске в больших пространствах дизъюнктивных выражений [ 1.1 ] . Суть стратегии такова. Для некоторого набора исходных дизъюнктивных выражений S можно указать подмножество T, называемое множеством поддержки. Для реализации этой стратегии необходимо, чтобы одна из резольвент в каждом опровержении имела предка из множества поддержки. Можно доказать, что если S - невыполнимый набор дизъюнктов, а S-T - выполнимый, то стратегия множества поддержки является полной в смысле опроверженияИсследования, связанные с доказательством теорем и разработкой алгоритмов опровержения резолюции, привели к развитию языка логического программирования PROLOG (Programming in Logic). PROLOG основан на теории предикатов первого порядка. Логическая программа - это набор спецификаций в рамках формальной логики. Несмотря на то, что в настоящее время удельный вес языков LISP и PROLOG снизился и при решении задач ИИ все больше используются C, C++ и Java, однако многие задачи и разработка новых методов решения задач ИИ продолжают опираться на языки LISP и PROLOG. Рассмотрим одну из таких задач - задачу планирования последовательности действий и ее решение на основе теории предикатов.

Задачи планирования последовательности действий

Многие результаты в области ИИ достигнуты при решении " задач для робота ". Одной из таких простых в постановке и интуитивно понятных задач является задача планирования последовательности действий, или задача построения планов.

В наших рассуждениях будут использованы примеры традиционной робототехники (современная робототехника во многом основывается на реактивном управлении, а не на планировании). Пункты плана определяют атомарные действия для робота. Однако при описании плана нет необходимости опускаться до микроуровня и говорить о датчиках, шаговых двигателях и т. п. Рассмотрим ряд предикатов, необходимых для работы планировщика из мира блоков. Имеется некоторый робот, являющийся подвижной рукой, способной брать и перемещать кубики. Рука робота может выполнять следующие задания ( U, V, W, X, Y, Z - переменные).

goto(X,Y,Z) перейти в местоположение X, Y, Z

pickup(W) взять блок W и держать его

putdown(W) опустить блок W в некоторой точке

stack(U,V) поместить блок U на верхнюю грань блока V

unstack(U,V) убрать блок U с верхней грани блока V

Состояния мира описываются следующим множеством предикатов и отношений между ними.

on(X,Y) блок X находится на верхней грани блока Y

clear(X) верхняя грань блока Х пуста

gripping(X) захват робота удерживает блок Х

gripping() захват робота пуст

ontable(W) блок W находится на столе


Рис. 3.8.Начальное и целевое состояния задачи из мира кубиков

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

Состояния мира кубиков представим в виде предикатов. Начальное состояние можно описать следующим образом:

start = [handempty, ontable(b),

ontable(c), on(a,b), clear(c),

clear(a)]

где: handempty означает, что рука робота Робби пуста.

Целевое состояние записывается так:

goal = [handempty, ontable(a),

ontable(b), on(c,b), clear(a),

clear(c)]

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

Прежде чем использовать эти правила, необходимо упомянуть о проблеме границ. При выполнении некоторого действия могут изменяться другие предикаты и для этого могут использоваться аксиомы границ - правила, определяющие инвариантные предикаты. Одно из решений этой проблемы предложено в системе STRIPS.

В начале 1970-х годов в Стэнфордском исследовательском институте (Stanford Research Institute Planning System) была создана система STRIPS для управления роботом. В STRIPS четыре оператора pickup, putdown, stack, unstack описываются тройками элементов. Первый элемент тройки - множество предусловий ( П ), которым удовлетворяет мир до применения оператора. Второй элемент тройки - список дополнений ( Д ), которые являются результатом применения оператора. Третий элемент тройки - список вычеркиваний ( В ), состоящий из выражений, которые удаляются из описания состояния после применения оператора.

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

unstack(A,B), putdown(A), pickup(C), stack(C,B)

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



Дата добавления: 2018-05-10; просмотров: 1310;


Поиск по сайту:

Воспользовавшись поиском можно найти нужную информацию на сайте.

Поделитесь с друзьями:

Считаете данную информацию полезной, тогда расскажите друзьям в соц. сетях.
Poznayka.org - Познайка.Орг - 2016-2024 год. Материал предоставляется для ознакомительных и учебных целей.
Генерация страницы за: 0.018 сек.