MGU y estandarización de variables - CNF

Question

He estado leyendo sobre la conversión de oraciones lógicas de primer orden a una forma normal conjuntiva y luego realizando resolución.

Uno de los pasos de convertir a CNF es estandarizar las variables: cambiar el nombre de todas las variables para que cada cuantificador tenga su propio nombre de variable único.

La mayor cantidad de unifier general es la unificación menos especializada de dos cláusulas.

Pregunta 1: He estado buscando encontrar un ejemplo que muestre cuáles son los problemas potenciales si no estandarizo las variables, pero todos los recursos en línea que encontré solo explican el "cómo" y no el "por qué". ¿Podría proporcionarme un ejemplo de un problema potencial?

Pregunta 2: El mismo problema que la primera pregunta. ¿Qué pasa si no usamos MGU y usamos un unifier más especializado? ¿Cuáles son los problemas potenciales? ¿Podría proporcionarme un ejemplo?

Mi sincero agradecimiento. Cripe

Answer 1

1. Ver esta respuesta - Es un ejemplo de un conjunto contradictorio de cláusulas donde no podemos derivar una contradicción sin cambiar el nombre de las variables. Tenga en cuenta que no es suficiente cambiar solo el nombre de las variables después de la conversión a CNF, tenemos que cambiar el nombre de las variables para ser distintas antes cada Aplicación de la regla de resolución. Puede verlo de la siguiente manera: una variable que aparece en dos cláusulas distintas tiene un significado diferente en cada uno de ellos, ya que están implícitamente cuantificadas universalmente. Si no cambiamos el nombre de la variable en una de las cláusulas, hacemos una suposición falsa de que la variable significa lo mismo en ambas cláusulas.

2. Al usar MGU, derivamos la cláusula más general en un paso de resolución. Si usamos algún unifier que sea más especializado que su MGU, la cláusula resultante es más débil. Esto significa que no inferimos todo el conocimiento que pudiéramos, y podemos perder una derivación de una cláusula vacía incluso si existe. Por ejemplo: begin {array} {c} p (x, y) lor q (y) lnot q (d) lnot p (c, d) end {array} si hacemos un Resuelto de las dos primeras cláusulas usando MGU que envía $ Y a D $, obtenemos $ P (x, d) $ y podemos continuar con la tercera cláusula. Si tomamos un unifier más débil, como uno que también envía $ X a D $, obtenemos $ P (D, D) $ y no podemos hacer un resolent con la tercera cláusula. Esto significa que el método ya no está completo.