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