12.8. Задачи, использующие равенства

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

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

В идеале хотелось бы иметь метод доказательства теорем, объединяющий преимущества обоих подходов. Можно было бы осуществить это двумя путями. Наиболее очевидный путь — дополнить множество исходных аксиом решаемой задачи аксиомами, определяющими равенство. Практически это мало приемлемо, так как при этом увеличиваются длина и число предложений в утверждениях. Тем самым значительно увеличивается число резолюций, которые можно провести, но они на самом деле не ведут к доказательству. Второй путь — включить в схему программы, использующей принцип резолюции, специальное правило вывода, которое должно применяться, когда возникает необходимость в операциях над равенствами. Чтобы это правило было совместимо с остальной частью устройства доказательства теорем, оно должно удовлетворять двум условиям: должно 1) работать с предложениями, в которых равенства выражены в виде атомов, и 2) быть операцией, превращающей два предложения в третье. Первое условие утверждает, что для выражения отношения равенства не нужны специальные типы данных, а второе гарантирует, что в ту же программу можно легко ввести механизмы применения как нового правила вывода, так и резолюции. Это специальное правило вывода, называемое парамодуляцией, было предложено с незначительными различиями несколькими авторами (Моррис, 1969; Робинсон и Вос, 1969; Сиберт, 1969). В основном наше изложение следует формулировке Робинсона и Воса.

Пусть А, В и т. д. будут множествами литералов, — термами (т. е. константами, переменными или функциональными выражениями). В дополнение к обычному определению атомов и литералов (т. е. атомов и их дополнений) будем записывать атомы равенства в виде (терм а равен терму (5). Разумеется, к термам можно применять подстановку.

Правило парамодуляции

Если для заданных предложений (или не имеющих общих переменных в общей части В выполняются условия

(i) C содержит терм ,

(ii) есть наиболее общий подстановочный частный случай

где — переменные соответственно из и

то надо построить предложение а затем заменяя а на для какого-то одного вхождения а в которое произошло от в Наконец, вывести

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

можно вывести

Несколько сложнее случай

Подстановка дает

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

то одно применение парамодуляции с подстановкой дает сначала

а затем или

или

Для получения же

требуется повторное применение парамодуляции.

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

девочки, назвавшейся принцессой. Пример математического характера можно найти в работе Робинсона и Воса (1969, стр. 140). Хотя наш пример можно считать необычным, он, в самом деле, нуждается в использовании отношений равенства для усиления исходных предложений из . В табл. 12.7 приведены соответствующие определения и исходные предложения.

Таблица 12.7. (см. скан) Определения и предложения для иллюстрации вывода при помощи парамодуляции

С помощью метода, изложенного в предыдущем разделе, можно удалить квантор существования из предложений Обозначим через сколемовские функции; тогда

Кванторы всеобщности в предложениях можно опустить. Проводя резолюцию а затем получаем

Затем осуществим парамодуляцию и выполнив тем самым подстановку в равенство. Это даст

В результате парамодуляции получаем

Наконец, парамодуляция приводит к предложению

Оно может служить тестом королевского происхождения.