2.3.3 Логическое программирование

В первом приближении логическое программирование - это использование дедуктивных процедур (процедур логического вывода) как механизма вычислений. Языки логического программирования являются декларативными в отличие от обычных “процедурных” языков”. В них в виде логических аксиом формулируются сведения о задаче и предположения, достаточные для ее решения. Сама задача формулируется как целевое утверждение, подлежащее доказательству. Таким образом, программа представляет собой множество аксиом, а вычисление - это конструктивный вывод целевого утверждения из программы. В логическом программировании (мы будем говорить о языке ПРОЛОГ) используется только одно правило вывода - резолюция.

Резолюция обладает важными свойствами - корректностью и полнотой. Резолюция корректна в том смысле, что если с ее помощью из множества формул S={F₁,...,F_k} и отрицания формулы R выводится пустой дизъюнкт, то справедливо F₁F₂...F_kR. Резолюция является полной в том смысле, что если R является логическим следствием множества формул S, то пустой дизъюнкт обязательно выводится из F₁F₂...F_kR. Однако, в 1936 году Черчем и Тьюрингом было доказано, что для логики предикатов не существует разрешающего алгоритма для проверки общезначимости (и, следовательно, невыполнимости) формул. Поэтому запустив процесс логического вывода, в общем случае мы не можем сказать, завершится ли он. Если R не является логическим следствием формул S, то алгоритм доказательства может никогда не завершиться в случае, если существует бесконечное число возможных резольвент, последовательно получаемых в процессе выполнения алгоритма доказательства. Однако, для предикатов с конечной областью определения, и тем более в логике высказываний, не только положительный, но и отрицательный ответ на вопрос о невыполнимости логической функции всегда будет получен методом резолюции в конечное время (за конечное число шагов).

Логический вывод в Прологе

Логика предикатов и понятие логического вывода были разработаны в первой половине нашего века, но только в конце 60-х были поняты огромные возможности логического вывода для построения непроцедурных алгоритмов, тогда же и были разработаны методы резолюции, алгоритм унификации, и в конце концов язык логического программирования ПРОЛОГ. Основной вклад в логическое программирование был сделан Аланом Робинсоном (Alan Robinson), Алайном Колмерауером (Alain Colmeraurer) и Робертом Ковальски (Robert Kowalski), причем он был сделан сравнительно недавно. В этом языке исходное множество формул, для которого ищется пустая резольвента, представляется в виде так называемых “дизъюнктов Хорна”. Хорновские дизъюнкты - это формулы одного из трех типов:

отрицание : (В1,...,Вn)

факт: А

импликация (правило): А(В1,...,Вm),

где А, В₁, ... - литеры - атомные высказывания или предикаты с отрицаниями или без них в нормальной предваренной форме только с (подразумеваемыми) кванторами всеобщности для всех переменных. Как мы видели из предыдущих разделов, любую логическую формулу можно привести к такому виду. Факты можно рассматривать как импликации, не имеющие посылок (антецедентов). Отрицания - как импликации, не имеющие следствий (консеквентов). Поэтому все дизъюнкты Хорна - это формулы вида А(В₁,...,В_m), которые просто являются другой записью импликации В₁...В_mА, и знак  здесь может читаться как "при условии, что". Все эти формулы представляются в виде дизъюнктов: В₁...В_mА, или просто множеством литер {А,В₁,...,В_m}, поскольку знак дизъюнкции подразумевается. Именно к этим дизъюнктам и применяются последовательные шаги метода резолюции.

Таким образом, все задачи логического вывода можно формулировать, пользуясь только дизъюнктами Хорна, и все те задачи, которые являются в принципе разрешимыми, можно решить с помощью метода резолюции. Рассмотрим несколько примеров из [GL88].

Пусть в нотации, близкой языку ПРОЛОГ, записана программа:

Программа_1::

1: птица(Х)  откладывает_яйца(Х), имеет_крылья(Х)

2: рептилия(Х)  откладывает_яйца(Х), имеет_чешую(Х)

3: откладывает_яйца(ворона)

4: откладывает_яйца(питон)

5: имеет_чешую(питон)

6: имеет_крылья(ворона)

7:?птица(ворона)

В первой строке стоит правило, которое можно понять так: любое животное является птицей при условии, что оно откладывает яйца и имеет крылья. Очевидно, что это просто предикат в предваренной нормальной форме с опущенным квантором всеобщности (потому здусь и следует читать: любое животное). Этот предикат задан здесь одним дизъюнктом (птица(Х), отладывает_яйца(Х), имеет_крылья(Х)), где атомные предикаты дизъюнкта просто перечисляются через запятую вместо того, чтобы перечисляться через знак дизъюнкции. Вторая строка - это правило, аналогично определяющее класс рептилий. Третья строка - “откладывает_яйца(ворона)” - это, факт, который мы считаем истинным. Часто подобные факты присоединяются к программе из базы данных. Последняя строка - это утверждение-вопрос, истинность которого процессор языка ПРОЛОГ пытается проверить с помощью метода резолюции, пользуясь фактами и правилами.