Пропозициональная логика в языке Prolog

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

В основе доказательства лежит рассуждение как объект знания. Мы признаем некоторое суждение, если располагаем подтверждением для него. Разновидностью подтверждения, которая нас интересует, является доказательство, отображаемое как дедукция с использованием правила вывода в форме.

где R — правило; Jj, — предпосылки (антецеденты) правила;

J — суждение, порождаемое правилом (консеквент). Мы можем прочитать это следующим образом:

Если J_x и … иJ_rv тоJ, если правило R верно.

Наиболее общим суждением является истинность высказывания А, записываемая как А истинно. Поскольку мы будем оперировать почти исключительно с истинностью высказываний, окончание истинно мы можем опустить. Другими примерами суждений высказываний являются А ложно, А истинно в момент t (субъект темпоральной логики) и К знает, А (К знает, что А истинно, субъект эпистемологии).

Рассмотрим простой пример логической программы в пропозициональной логике, состоящей из следующих высказываний (после символа % размещаются комментарии).

volkhov —> windy % В Волхове ветрено.

kronstadt —> windy % В Кронштадте ветрено.

kronstadt —> Petersburg % Кронштадт в Петербурге.

Petersburg —> rainy % В Петербурге дождливо.

rainy л windy —> umbrellauseless % Если ветрено и дождливо, то зонтик бесполезен.

kronstadt % Высказывание «Кронштадт» истинно Доказательство в нотации математической логики выглядит следующим образом:

Здесь из истинности импликации kronstadt —> windy и атома kronstadt вытекает истинность атома windy. Далее, если истинны импликация kronstadt —" Petersburg и атом kronstadt, то истинен атом Petersburg.

Теперь, если истинны импликация Petersburg —> rainy и атом Petersburg,, то истинен атом rainy:

Наконец, если истинны импликация rainy л windy —> umbrella_ useless и атомы rainy и windy, то истинен атом umbrella juseless:

Теорема доказана. Это же доказательство можно записать в линейной форме:

• 1. kronstadt аксиома
• 2. kronstadt —> windy аксиома
• 3. windy обратный вывод из п. 1, 2
• 4. kronstadt —> Petersburg аксиома
• 5. Petersburg обратный вывод из п. 1,4
• 6. Petersburg —" rainy аксиома
• 7. rainy обратный вывод из и. 5, 6
• 8. windy л rainy —> umbrella juseless аксиома
• 9. umbrella juseless обратный вывод из п. 3,7,8

В самом начале цель: [umbrellajuseless].

Первый атом в цели, umbrella_useless, не является аксиомой. Единственное правило в программе, которое может быть использовано для порождения umbrella juseless, это windy л rainy —> —> umbrella juseless. Заменяем текущую цель на [windy, rainy].

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

volkhov —> windy kronstadt —> windy

Используем сначала первое правило и заменяем цель на [volkhov, rainy].

Первый атом цели, volkhov, не является аксиомой, и в программе нет правил, которые могли быть использованы, чтобы породить volkhov. Иными словами, мы не находимся в Волхове. Следовательно, проверка данной цели неудачна, и выполняется бэктрекинг (возврат к другой альтернативе). Мы восстанавливаем текущую цель |windy, rainy].

Мы уже видели, что первый атом цели windy не является аксиомой, а первое правило volkhov —> windy не порождает решения для windy. Следовательно, мы пытаемся применить второе правило, удовлетворяющее цели windy:

kronstadt —> windy

Заменяем текущую цель на [kronstadt, rainy].

Первый атом цели, kronstadt, это аксиома. Следовательно, эта подцель решена, мы удаляем ее и списка цели и заменяем текущую цель на [rainy].

Продолжая таким образом, мы получаем успешные решения:

Текущая цель: [rainy]. Текущая цель: [Petersburg]. Текущая цель: [kronstadt]. Текущая цель: [].

Теперь поиск породил пустой список для текущей цели. Это означает, что поиск цели umbrella juseless завершился успешно (рис. 1.3).

Рис. 13. Иллюстрация к приводимому примеру программы в пропозициональной логике

То же самое на языке Prolog выглядит так:

windy volkhov.

windy kronstadt.

Petersburg kronstadt.

rainy Petersburg.

umbrella_useless windy, rainy.

kronstadt.

Запрос может выглядеть следующим образом:

?- umbrella_useless.

Решение задачи на языке Prolog состоит в том, что искомые цели помещаются в стек целей. Далее выполняется поиск фактов в базе знаний, которые соответствуют цели. Если такие факты находятся, то они удаляются из стека целей. Если вместо факта.

Prolog находит правило, то условия правила (антецеденты) помещаются в стек целей, т. е. Prolog сам себе устанавливает новые цели. Поиск решения завершается тогда, когда стек целей становится пустым. На рис. 1.4 приведено дерево решений для данной задачи.

Рис. 1.4. Дерево решений для цели umbrella useless

При попытке найти решение здесь мы сталкиваемся с тем, что у нас нет данных относительно Волхова, находимся ли мы в этом городе или нет. Попытка сопоставить утверждение windy с утверждением volkhov потерпит неудачу. Здесь мы сталкиваемся с ситуацией, когда отсутствие данных приводит к отрицанию результата (negation as failure). Это связано с тем, что в бинарной логике отсутствие положительного результата равносильно отрицательному результату.

Модифицируем программу следующим образом:

windy volkhov.

windy kronstadt.

Petersburg kronstadt.

rainy Petersburg.

umbrella_useless windy, rainy.

kronstadt.

volkhov fail.

Последний предикат отрицает факт нахождения в Волхове. Теперь запрос.

?- umbrella useless будет завершаться успехом. В дальнейшем мы рассмотрим, как различать отрицание и неудачу поиска решения. Заметим, что в данном контексте мы не детализируем смысл утверждений Petersburg и volkhov. Это может быть наше местоположение либо просто указание географической точки. В первом случае мы не запрещаем одновременное нахождение в двух местах. Добавим в стек целей признак истинности (рис. 1.5). Первоначально этот признак устанавливается в 1 (истина). Если в процессе поиска решений встречается факт, явно отрицающий цель, то признак устанавливается в 0 (ложь) и доказательство остальных целей в стеке можно прекратить, поскольку это не имеет смысла.

Рис. 1.5. Дерево решений для модифицированной программы.

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