Segundo Parcial del 1er Cuatrimestre de 2022

Ejercicio 2)

Estas son las cláusulas resultantes, 1 y 2 corresponden a "Para todo x par existe un impar mayor que él"; 3 y 4 a la "Para todo x impar existe un par mayor que él", 5 a "La relación de mayor es transitiva" y 6 y 7 al goal (no olvidarse de negarlo).

1: {¬par(X1), mayor(f(X1),X1)}
2: {¬par(X2), ¬par(f(X2))}
3: {par(X3), mayor(g(X3),X3)}
4: {par(X4), par(g(X4))}
5: {¬mayor(X5,Y5), ¬mayor(Y5,Z5), mayor(X5,Z5)}
6: {par(c)}
7: {¬mayor(Y7,c), ¬par(Y7)}

De 6 y 1 con {X1 ← c}:
  8: {mayor(f(c),c)}

De 8 y 7 con {Y7 ← f(c)}:
  9: {¬par(f(c))}

De 9 y 3 con {X3 ← f(c)}:
  10: {mayor(g(f(c)),f(c))}

De 9 y 4 con {X4 ← f(c)}:
  11: {par(g(f(c)))}                         //Ya tenemos f(c)>c impar y g(f(c))>f(c) par.

De 5 y 10 con {X5 ← g(f(c)), Y5 ← f(c)}:
  12: {¬mayor(f(c),Z5), mayor(g(f(c)),Z5)}   //Vamos a probar por transitividad que g(f(c))>c

De 12 y 8 con {Z5 ← c}:
  13: {mayor(g(f(c)),c)}

De 13 y 7 con {Y7 ← g(f(c))}:
  14: {¬par(g(f(c)))}                        //Vimos antes que g(f(c)) era par!

De 14 y 11 con {}:
  15: □