En la demostración del teorema de resolución, normalmente se supone que las variables en diferentes cláusulas son distintas. Esto no es algo que sucede automáticamente; requiere un código adicional significativo y computación para implementar. Dado eso, estoy buscando un caso de prueba para ello.
El problema es que, en todos los casos de prueba que he probado hasta ahora, no hay diferencia. Presumiblemente solo importa en casos extremos inusuales. Como dice Wikipedia , "las variables en diferentes cláusulas son distintas ... Ahora, unificar Q (X) en la primera cláusula con Q (Y) en la segunda cláusula significa que X e Y se convierten en la misma variable de todos modos".
¿Existen casos de prueba conocidos que realmente den una respuesta incorrecta si diferentes cláusulas usan las mismas variables?
fuente