Разные переменные для разных предложений

10

При доказательстве теоремы разрешения обычно предполагается, что переменные в разных разделах различны. Это не то, что происходит автоматически; это требует значительного дополнительного кода и вычислений для реализации. Учитывая это, я ищу тестовый пример для него.

Проблема в том, что во всех тестовых случаях, которые я пробовал до сих пор, это не имеет значения. Предположительно это имеет значение только в необычных крайних случаях. Как говорит Википедия , «переменные в разных предложениях различны ... Теперь объединение Q (X) в первом предложении с Q (Y) во втором предложении означает, что X и Y в любом случае становятся одной и той же переменной».

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

rwallace
источник

Ответы:

6

Изменить: я нашел лучший пример. Рассмотрим следующие пункты: Очевидно, этот набор положений противоречив. Но без переименования переменных единственная возможная резольвента - это и никакие другие резольвенты невозможны - все это приводит к замене на , что невозможно. P(f(x))f(x)x

¬P(x)P(f(x))P(x)¬P(f(f(x)))
P(f(x))f(x)x

Изменить: рассмотреть смысл пунктов. Каждое предложение неявно универсально количественно. Так что значение его переменных ни к чему не привязано. Теперь предположим, что у вас есть два предложения, каждое из которых содержит . Если вы выполняете разрешение без переименования x в одном из них, тогда вы добавляете значение x, которого у него нет: вы говорите, что x означает одно и то же в обоих пунктах, что неверно. Если у вас нет четких переменных в ваших предложениях, разрешение даст вам слишком слабые выводы.xxxx


(Оригинальный ответ.) Например, у нас есть 4 предложения:

  1. AB(x)
  2. ¬AC(x)
  3. ¬B(c)
  4. ¬C(d)

где - переменные, а постоянные. Если мы выполним разрешение для первых двух без переименования , мы получим . Мы можем продолжить с чтобы получить но теперь мы не можем решить его с .c , d x B ( x ) C ( x ) ¬ B ( c ) C ( c ) ¬ C ( d )x,yc,dxB(x)C(x)¬B(c)C(c)¬C(d)

С другой стороны, если мы переименуем во во втором, чтобы получить непересекающийся набор переменных, мы получим с первого шага разрешения и мы можем получить пустое предложение, используя и .y B ( x ) C ( y ) ¬ B ( c ) ¬ B ( d )xyB(x)C(y)¬B(c)¬B(d)

Петр Пудлак
источник
Когда я пытаюсь сделать это в моем средстве проверки с отключенными различными переменными, он разрешает с чтобы дать , аналогично получает и, следовательно, пустое предложение, так что конечный результат остается тем же. Я что-то пропустил? ¬ B ( c ) A ¬ AB(x)¬B(c)A¬A
Rwallace
@rwallace Отсутствие различных переменных не означает, что вы не можете получить пустое предложение, просто то, что методы не завершены. Если вы всегда переименовываете переменные, тогда не имеет значения, в каком порядке вы выбираете предложения, вы всегда получите пустое предложение, если исходный набор неудовлетворителен - метод завершен. Но если вы не переименуете переменные, то (как показывает пример) порядок внезапно имеет значение - некоторые последовательности дериваций не найдут пустое предложение. И проверяющий не может заранее «сказать», какая последовательность производных является правильной.
Петр Пудлак
Но разве это не тот случай, когда завершенный метод должен в конечном итоге попробовать все возможные деривации (если он сначала не найдет пустое предложение)? Чтобы быть уверенным, что нет никакой гарантии, он попробует деривации, которые я упомянул раньше, чем те, которые вы упомянули, но когда те, которые вы упомянули, терпят неудачу из-за отсутствия различных переменных, те, которые я упомянул, все еще открыты, и полный метод должен вернуться и попробовать те, рано или поздно?
Rwallace
Ваше приложение о значении положений в аннотации имеет смысл, но мне кажется, если это так, тогда должна быть возможность найти контрольный пример, что-то, что я могу передать доказателю и заставить его дать неправильный ответ, если функция различных переменных отключена. Я просто пока не смог найти такой контрольный пример.
Rwallace
@rwallace Зачем тебе это делать? Разрешение является полным методом, и вы знаете, что при любых обстоятельствах необходимо выполнять разрешение для каждой пары предложений только один раз. Вы предлагаете в конечном итоге попробовать все возможные последовательности, как продолжить возврат. Это приведет к действительно огромному увеличению сложности алгоритма, даже отдаленно не сопоставимому с простым переименованием переменных на каждом шаге.
Петр Пудлак