Точно Не проект 2 / Не books / Источник_1

R(nil,nil)

Рисунок 4.8 – Модифицированное дерево доказательства для yR(nil, y)

Чтобы выполнить доказательство для случая n>0 , сформулируем новое дополнительное индуктивное утверждение: “для любого непустого списка х его хвост, получаемый с помощью функции cdr(x), можно отсортировать“. Если допустить, что у нас уже есть функция sort, которая может выполнить сортировку списка, то указанное утверждение можно записать в виде дизъюнкта R(cdr(x),sort(x)). Добавим его к множеству аксиом Ф0. Также добавим к множеству Ф0 очевидное предложение

R(cons(car(x),cdr(x)), y) R(x, y),

которое после исключения знака импликации примет вид

R(cons(car(x),cdr(x)), y) R(x, y).

Если учесть, что cons(car(x), cdr (x))=x, то последнее предложение представляет собой тавтологию, и ее добавление не создает противоречия.

Модифицированное дерево доказательства для предположенияx yR(x, y)изображено на рисунке 4.9.

Заменив в ответном утверждении функцию а на переменную х, полу-

чим

R(x, merge(car(x),sort(cdr(x)))).

Объединяя результаты доказательства для n=0 и n>0, получаем рекурсивную программу упорядочения списка чисел:

4.1.7. Принцип резолюции и система STRIPS

Система STRIPS (от англ. Stanford Research Institute Problem Solver –

решатель задач Стэнфордского исследовательского института) относится к классу решателей задач и представляет собой программу управления роботом, который способен целенаправленно передвигаться в среде с подвижными препятствиями [44]. Задачу перемещения (навигации) робота можно рассматривать как задачу поиска в пространстве состояний. Описание задачи состоит из:

-описания состояния (модели) среды, в которой находится робот;

-описания набора имеющихся операторов, каждый из которых преобразует модель среды;

-описания целевого состояния.

Пространство состояний описывается множеством ППФ. Например, состояние, при котором робот находится в точке а, а контейнеры k1 и k2 -- в точках b, c, d , можно описать с помощью следующих ППФ:

ATR(a);

AT(k1,b);

AT(k2,c);

AT(k3,d).

Операторы представляются в виде операторных схем, которые характеризуются именем, списком параметров и описаниями. Описания операторных схем выполняются на языке исчисления предикатов и включают в себя условия применимости оператора, список вычеркиваний и список добавлений. Например, операторная схема goto(m,n) определяет обобщенное действие, связанное с переходом робота из точки m в точку n. Переменные m и n рассматриваются как параметры схемы, в которые подставляются константы, задающие возможные позиции робота. Операторная схема порождает конкретные операторы, которые преобразуют среду. Операторная схема goto(m,n) может быть применена только в том случае, если робот находится в точке m. Поэтому условия ее применимости записываются в виде ATR(m). В результате применения данной операторной схемы робот перейдет из точки m в точку n . Это приведет к изменению состояния среды. Теперь, во множество ППФ, описывающих состояние среды, необходимо добавить утверждение ATR(n) и исключить из него утверждение ATR(m). Следовательно, список добавлений должен содержать предикат AТR(n) , а список вычеркиваний – предикат ATR(m). Таким образом, описание рассматриваемой операторной схемы будет следующим:

Кроме этого, потребовалось внести дополнение в процедуру доказательства. Пусть D1 и D2 два дизъюнкта, которые образуют резольвенту D, и={t/p} некоторая подстановка, используемая при получении D, где t – терм, поставляемый вместо параметра p. Дополнение заключаются в том, что р заменяется на t во всех дизъюнктах, являющихся производными от D.

В системе STRIPS поиск решения начинается с попытки доказательства того, что целевая ППФ G0 следует из множества формул М0, определяющих исходное состояние (модель) среды. Для этого система доказывает невыполнимость множества {M0 G0}. Если это доказано, то исходное состояние удовлетворяет цели, и задача решена. Если же невыполнимость множества{M0 G0}не установлена, то образуется незавершенный вывод.

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

Подцель в системе STRIPS обрабатывается аналогично цели. Иными словами, система теперь пытается установить невыполнимость множест-

ва{M0 G1}, где G1 – новая подцель, соответствующая условиям применимости выбранного оператора.

Если на данном шаге устанавливается выводимость ППФ G1 из М0, то это означает, что выбранный оператор, например ОР1, может быть применен к состоянию M0. Применив частный вид оператора ОР1, полученного

входе доказательства теоремы М0 G1, система преобразует состояние М0

вновое состояние М1. После этого система вновь попытается установить выводимость G0, но теперь уже из множества формул, описывающих состояние М1. Если же в ходе доказательства теоремы М0 G1 будет полу-

чено незавершенное доказательство, то вновь будет выполняться поиск оператора, обеспечивающего такое изменение М0, чтобы можно было продолжить доказательство. При этом формируется новая подцель, например G2 , а подцели G1 и G0 отодвигаются на второй план. Указанный процесс повторяется, пока не будет доказана цель G0.

Описанный процесс показывает, что, до момента получения окончательного решения, неизвестно какое место в этом решении займет тот или иной оператор. Например, ОР1 может быть применен к исходной модели среды М0 или его применение может быть отложено до момента, когда другой оператор, рассматриваемый после ОР1, преобразует модель к необходимому виду. Такая стратегия сочетает в себе преимущества прямого и обратного поиска. Она дает возможность решить основные подзадачи методом поиска вперед. Затем, чтобы решить вспомогательные подзадачи, возникающие при соединении вместе отдельных частей решения, осуществляется обратный поиск.

Рассмотрим описанные этапы работы системы SRTIPS на примере. Пусть требуется, чтобы робот переместил три контейнера k1,k2 и k3 в одну точку. Исходная модель среды задана множеством формул:

M0 {ATR(a), AT(k1,b), AT(k2,c), AT(k3,d)}.

Целевая формула в этом случае запишется в виде (4.1). Ее отрицание будет иметь вид:

G0 AT(k1,x) AT(k2,x) AT(k3,x) .

Cистеме доступны следующие операторы: goto(m,n) и push(k,m,n). Оператор goto(m,n) описан выше, а оператор push(k,m,n) обеспечивает перемещение объекта k из позиции m в позицию n. Описание данного оператора задается следующим образом:

Решение задачи будем сопровождать построением дерева поиска

(рисунок 4.10).

Сначала предпринимается попытка найти противоречие для множества {M0 G0}(вершина (M0,(G0)) на рисунке 4.10). Необходимые построения для данного шага изображены на рисунке 4.11.

Образовавшееся неполное доказательство представляет собой различие текущего и целевого состояний среды. Единственным оператором, способным уменьшить данное различие, является push(k,m,n). В его списке добавлений имеется дизъюнкт АТ(k,n), который позволяет продолжить доказательство. В зависимости от подстановок, выполняемых в параметры k и n, возможны шесть вариантов продолжения доказательства. Каждая из подстановок порождает частный вид оператора. Например, подстановка1 {k2/k,b/n}дает частный оператор OP1: push(k2,m,b).

литерал ATR(a) , который при подстановке 3={a/m} образует с литералом

ATR(m) контрарную пару. Следовательно, система STRIPS может применить оператор ОР2, имеющий конкретный вид goto(a,c), к состоянию М0. В результате получается новое состояние

M1 {ATR(c),AT(k1,b),AT(k2,c),AT(k3,b)},

и на дереве поиска формируется новая вершина (M1,(G1,G0 )) (рисунок 4.10). Далее система устанавливает, что множество {M1 G1}является противоречием, если выполняется подстановка 4={c/m}. Поэтому она применяет оператор ОР1 с учетом подстановки 4, т. е. push(k2,c,b). В итоге, получается новое состояние:

M2 {ATR(b),AT(k1,b),AT(k2,b),AT(k3,d)}.

На дереве поиска формируется новая вершина (M2,(G0)).

Затем система STRIPS вновь пытается вывести целевую формулу G0, но теперь уже из множества М2. Дальнейшее решение задачи будет протекать так же, как описано выше. Окончательное решение получается в форме:

{goto(a,c), push(k2,c,b), goto(b,d), push(k3,d,b)}.

В заключение отметим, что в системе STRIPS имеется большее число операторов, и она умеет работать с более сложной моделью среды.

4.1.8. Принцип резолюции и язык Пролог

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

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

Имена предикатов и констант в Прологе записывают строчными буквами. Имена переменных начинаются с большой буквы или знака подчеркивания. Конкретный список, состоящий из элементов a, b, c, d , записывается на языке Пролог в следующем виде [a,b,c,d]. Список в Прологе может задаваться с помощью переменных, например, [H|T], где Н – голова списка, Т – хвост списка.