Введение. Логическое программирование

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

Методические указания к выполнению лабораторных работ для студентов специальности 220400 – Программное обеспечение вычислительной техники и автоматизированных систем

Белгород 2000

Введение

Осознание того, что вычисление – часть случайного логического вывода привело к возникновению логического программирования [4], первая реализация которого была осуществлена в семидесятые годы в виде системы Пролог [1, 2, 9]. Суть идеи – представить в качестве программы формальное описание предметной области, а затем сформулировать необходимую для решения задачу в виде цели или утверждения. Построение же решения этой задачи в виде вывода в этой системе предложить самой машине. Последнее возможно, поскольку нужный алгоритм решения (поиска) осуществляется решателем, строящим вывод по определенной стратегии [3, 8]. При такой постановке основная задача программиста сводится к описанию предметной области в виде системы логических формул и отношений на них, которые с достаточной степенью полноты описывают задачу. Этот подход стал возможен благодаря тому, что были получены достаточно эффективные методы автоматического поиска доказательств [8].

Проиллюстрируем вышесказанное, воспользовавшись исчислением высказываний [8]. Дадим формальное описание предметной области:

F1: Если жарко и сыро, то будет дождь.

F2: Если сыро, то жарко база знаний

F3: сейчас сыро

Воспользуемся обозначениями:

Р – жарко, Q – сыро, R – будет дождь,

тогда

F1 =PÙQ®R

F2 =Q®P формальное описание базы знаний

F3: Q

и зададимся вопросом-целью:

будет ли дождь?

Решим поставленную задачу, воспользовавшись правилом вывода modus ponens: A, A ® B => B (если верно А и A®B, то верно и B). Тогда Q, Q ® P => P, т. е. верно P.

Но тогда QÙP, QÙP ® R => R, т.е. верно R. То есть, поставленная задача решена, ответ – будет дождь.

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

E (x, y) – числа x и y равны между собой

f (x) – число, следующее за числом x

g (x) – число, предшествующее числу x

1. За каждым числом существует другое

А (" х)(($ у)(Е(у, f (x)))Ù" z)(E(z, f (x)))®E(y, z)

2. Нуль является крайним числом

А ~ ($ x)(E(0, f (x)))

3. Существует один предыдущий элемент для всех чисел кроме нуля.

А (" х)(~E(x,0)®(($ y)(E(y, g (x))Ù(" z)(E(z, g (z)) ® E(y, z)))

Использование правила вывода modus ponens позволяет показать возможность достижения цели – доказательства теорем. На практике обычно используется более эффективные с точки зрения вывода методы доказательства теорем.

Один из таких методов – метод резолюции [3] – позволяет реализовать на практике концепцию логического программирования, согласно которой вычислительная программа может быть записана при помощи логических формул, играющих роль аксиом, а её вычисление представлено в виде доказательства формулы-запроса.

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

Правило резолюций в простейшем случае имеет вид

ØA, A ® B => ØB,

результат называется резольвентой, а само правило modus tollens.

Для доказательства выводимости некоторой формулы G из формул F₁, F₂,..., F_n, достаточно доказать истинность формулы F₁ Ù F₂... Ù F_n ® G.

Теорема. F₁ Ù F₂... Ù F_n ® G <=> F₁ Ù F₂... Ù F_n Ù Ø G – противоречиво

То есть для доказательства G достаточно опровергнуть ØG. Это так называемое доказательство от противного или reductio ad absurdum.

Логическое программирование является описательным (декларативным). В нем используются утверждения трех видов: факты, правила, вопросы. Воспользуемся примером Пролог-программы, приведенной в работе [3] (рекомендуем рассмотреть работу интерпретатора, воспользовавшись алгоритмом, описанным на стр. 8):

вор(питер).

любит(мэри, шоколад).

любит(мэри, вино)

любит(питер, деньги).

любит(питер, X):- любит(X, вино).

может_похитить(X, Y):- вор(X), любит(X, Y).

и опишем работу интерпретатора для цели

? может_похитить(питер, X).

то есть вопрос «что может похитить Питер?».

Интерпретатор отыщет последнее правило программы и унифицирует цель с его левой частью, при этом

X = питер, а Y = Z,

вместо старой цели появятся две новые подцели:

? вор(питер), любит(питер, Z).

Первая подцель достижима, поскольку она унифицируется с фактом в программе: вор(питер).

Вторая подцель: любит(питер, Z) будет унифицирована с фактом любит(питер, деньги), при этом

Z = деньги.

Поскольку и эта цель достижима, интерпретатор выдаст ответ Y = деньги. То есть Питер может_похитить деньги.

Интерпретатор продолжит поиск других целей и расторгнет унификацию цели любит(питер, X) с фактом любит(питер, деньги). Взамен этого цель любит(питер, X) будет унифицирована с правой частью правила, расположенного в пятой строке программы. Эта унификация означает, что X = Z и вместо старой цели любит(питер, X) будет выставлена цель любит(Z, вино), поскольку X = Z. Эта цель будет достигнута, поскольку она унифицируется с фактом, находящимся в третьей строке – любит(мэри, вино). В результате Z = мэри и интерпретатор выдаст ещё один ответ Z = мэри, то есть питер может_похитить мэри.

В заключение отметим, что Пролог позволяет решать задачи, относящиеся к искусственному интеллекту:

- общение с ЭВМ на естественном языке;

- формальные вычисления;

- написание компиляторов;

- работа с базами данных;

- экспертные системы и другие.

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