Логическое программирование в ограничениях
В приведенном выше описании прямого логического вывода (раздел 9.3) было показано, как можно представить задачи удовлетворения ограничений (Constraint Satisfaction Problem— CSP) в виде определенных выражений. Стандартный язык Prolog позволяет решать подобные задачи точно таким же способом, как и алгоритм поиска с возвратами, приведенный в листинге 5.1.
Поскольку поиск с возвратами предусматривает полный перебор областей определения переменных, он может применяться только для решения задач CSP с конечными областями определения. В терминах Prolog это можно перефразировать таким образом, что для любой цели с несвязанными переменными должно существовать конечное количество решений. (Например, цель dif f (q, sa), которая определяет, что штаты Квинсленд и Южная Австралия должны быть окрашены в разные цвета, имеет шесть решений, если допускается применение трех цветов.) Задачи CSP с бесконечными областями определения (например, с целочисленными или вещественными переменными) требуют применения совсем других алгоритмов, таких как распространение пределов или линейное программирование.
Приведенное ниже выражение выполняется успешно, если подставленные в него три числа удовлетворяют неравенству треугольника.
triangle(X,Y,Z) :-X> = 0, Y>=0, Z> = 0, X+Y>=Z, Y+Z>=X, X+Z>=Y.
Если системе Prolog передан запрос triangle (3 , 4, 5), он будет выполнен безукоризненно. С другой стороны, после передачи запроса triangle (3 , 4, Z) решение не будет найдено, поскольку подцель z>=0 не может быть обработана системой Prolog. Возникающая при этом сложность состоит в том, что переменные в системе Prolog должны находиться только в одном из двух состояний: несвязанные или связанные с конкретным термом.
Связывание переменной с конкретным термом может рассматриваться как крайняя форма ограничения, а именно как ограничение равенства. Логическое программирование в ограничениях (Constraint Logic Programming — CLP) позволяет ограничивать, а не связывать переменные. Решением для программы в логике ограничений является наиболее конкретное множество ограничений, налагаемых на переменные запроса, которое может быть определено с помощью базы знаний. Например, решением запроса triangle (3, 4, Z) является ограничение 7>=Z>=1. Программы в стандартной логике представляют собой частный случай программ CLP, в которых ограничения решения должны быть не ограничениями сравнения, а ограничениями равенства, т.е. связываниями.
Системы CLP включают различные алгоритмы решения задач с ограничениями для таких вариантов ограничений, которые разрешены к использованию в языке.
Например, система, позволяющая использовать линейные неравенства с переменными, имеющими вещественные значения, может включать алгоритм линейного программирования для решения этих ограничений. Кроме того, в системах CLP принят гораздо более гибкий подход к решению запросов стандартного логического программирования. Например, вместо использования поиска в глубину, слева направо, с возвратами, в них может применяться любой из более эффективных алгоритмов, описанных в главе 5, включая эвристическое упорядочение конъюнктов, обратный переход, определение условий формирования множества отсечения и т.д. Поэтому в системах CLP сочетаются элементы алгоритмов удовлетворения ограничений, логического программирования и дедуктивных баз данных.
Кроме того, системы CLP позволяют воспользоваться преимуществами различных методов оптимизации поиска в задачах CSP, описанных в главе 5, таких как упорядочение переменных и значений, предварительная проверка и интеллектуальный возврат. В частности, разработаны проекты нескольких систем, позволяющих программисту получить больший контроль над порядком поиска для логического вывода. Например, язык MRS [539], [1321] позволяет программисту-пользователю записывать метаправила для определения того, какие конъюнкты должны быть опробованы в первую очередь. Например, пользователь может сформулировать правило с указанием, что в первую очередь следует пытаться достичь цели с наименьшим количеством переменных, или оформить характерные для проблемной области правила, касающиеся конкретных предикатов.
Последнее из трех рассматриваемых в данной главе семейств логических систем основано на резолюции. Как было показано в главе 7, пропозициональная резолюция — это полная процедура логического вывода для пропозициональной логики на основе опровержения. В этом разделе будет показано, как распространить резолюцию на логику первого порядка.
Проблема существования полных процедур доказательства всегда является предметом непосредственного внимания математиков. Если бы удалось найти полную процедуру доказательства для математических утверждений, это повлекло бы за собой два последствия: во-первых, вывод всех заключений мог бы осуществляться механически; во-вторых, всю математику можно было бы построить как логическое следствие некоторого множества фундаментальных аксиом. Поэтому вопрос о полноте доказательства стал в XX веке предметом наиболее важных математических работ. В 1930 году немецкий математик Курт Гёдель доказал первую теорему о полноте для логики первого порядка, согласно которой любое высказывание, являющееся следствием заданных аксиом, имеет конечное доказательство. (Но никакая действительно применимая на практике процедура доказательства не была найдена до тех пор, пока Дж.Э. Робинсон не опубликовал в 1965 году алгоритм резолюции.) В 1931 году Гёдель доказал еще более знаменитую теорему о неполноте. В этой теореме утверждается, что любая логическая система, которая включает принцип индукции (а без этого принципа удается построить лишь очень малую часть дискретной математики), обязательно является неполной. Поэтому существуют такие высказывания, которые следуют из заданных аксиом, но в рамках данной логической системы для них невозможно найти конечное доказательство. Иголка действительно может быть в метафорическом стоге сена, но ни одна процедура не позволяет гарантировать, что она будет найдена.
Несмотря на то, что теорема Гёделя о неполноте устанавливает определенные пределы, программы автоматического доказательства теорем на основе резолюции широко применялись и применяются для обоснования математических теорем, включая несколько таких теорем, для которых до сих пор не было известно доказательство. Кроме того, программы автоматического доказательства теорем успешно использовались для проверки проектов аппаратных средств, формирования логически правильных программ, а также во многих других приложениях.