3.10.8. Язык Пролог и применение метода резолюции

Начиная с 1972 г. А. Кольмрауер разрабатывал со своей группой сотрудников в Марселе систему автоматического доказательства, построенную на базе логики первого порядка и методе Эрбрана—Робинсона. Для задания какой-либо задачи системе в терминах предикатов пользователь системы применял язык Пролог, причем система автоматически выдавала ответ (если он существовал), используя для этого унификацию и метод резолюции. Таким образом, Пролог может рассматриваться как декларативный язык, где единственными входными данными является формальное определение задачи. Так как пользователь заинтересован в эффективном решении своей задачи, то для него важно получение этого решения в явном виде и с этой точки зрения доказательство, основанное на опровержении специальным образом сконструированного предложения, получаемого методом резолюции, не является для него достаточным. Поэтому в 1969 г. для устранения этого недостатка Грин предложил ввести в исходный набор предложений “ответный” предикат, связанный с заключением:

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

Предположим, что требуется произвести вызов некоторого лица по телефону. Наши данные будут представлены в виде четырех предикатов т. е. надо соединить по телефону лицо Р по номеру телефона Лицо х находится в месте причем место имеет номер телефона т. Предположим, что Пьер хочет навестить своего друга Жана.

Тогда означает, что лицо у посетило лицо Следовательно, мы имеем для начальной точки, что (Пьер, Жан).

Теперь следует отразить полезные свойства используемых предикатов: если у посетило и если находится в то, следовательно, у также в (предложение Если Р находится в и если имеет номер телефона можно соединить по телефону Р с номером (предложение

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

Обработав эти предложения, Пролог непосредственно дает ответ 4654-32-10.

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

Выходной предикат становится здесь единственным литералом, причем ответ печатается системой.

Ответ, выдаваемый Прологом, может быть не только константой, но и формальной переменной, как, например, в следующем случае: если х является “отцом” для у и если является “дедом” для и все имеют Кто является “отцом” некоего

Здесь исходные условия представляются в следующем виде:

что приводит к следующим резолюциям:

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

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

Пусть, например, суть предикат, который имеет следующий смысл: ящик — бананы — у определяют состояние Тогда

— состояние, достигаемое роботом, переходящим от выходя из состояния

— состояние, достигаемое роботом, передвигающим ящик от начиная с состояния

— состояние, достигаемое роботом, взбирающимся на ящик, из состояния

а, Ь, с — первоначальные позиции робота, бананов, ящика (состояние );

— предикат, отражающий тот факт, что робот может достать бананы из состояния

Исходные предложения имеют следующий смысл. Робот может:

идти к ящику

двигать ящик

взобраться на ящик

(первоначальное состояние)

взять бананы

(отрицание цели) — вывод

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

Начиная с исходной позиции, робот идет от а к ящику с, который он двигает в под бананы, и теперь ему остается только взобраться на него