Ejemplo del mundo real de la unificación en la lógica de primer orden?

Question

Sé que esto es solo parte de una pregunta de programación, pero por el momento, estoy haciendo un poco de programación lógica. Una cosa que todavía no entiendo correctamente es la unificación en la lógica de primer orden.

He leído el Wikipedia article y es más o menos claro que el propósito es buscar un término que unifica dos oraciones ... También hay ejemplos en este artículo, pero simplemente no entiendo por qué esto debería ser útil . ¿Alguien puede dar un ejemplo con objetos del mundo real en lugar de A, B, C ,, etc.? Espero que esto me ayude a entender. Gracias

Answer 1

Si está viendo ejemplos del mundo real donde la unificación es utilizada y útil, eche un vistazo a las gramáticas basadas en la unificación que se utilizan en lingüística computacional, por ejemplo, HPSG y LFG. En la superficie, esto se parece a otro sabor de unificación, pero en realidad son lo mismo.

La gramática basada en unificación se puede considerar como una CFG (gramática libre de contexto) donde las producciones se amplían con la unificación. Cada término en el CGF obtiene una MAV (matriz de valor de atributo), que es un gráfico acíclico dirigido de características y valores. La idea aquí es algo similar a las gramáticas de atributos utilizados en los compiladores.

Imagínese este juguete gramática:

S -> NP VP 
NP -> Kim 
NP -> The cats 
VP -> V NP 
V -> see 
V -> sees 

Tenemos una ligera overgeneration aquí en el acuerdo:

* Los gatos ve Kim [S [NP Los gatos] [VP [V ve] [ NP Kim]]]

con el fin de solucionar este problema podríamos refinar el CFG para incluir la noción de acuerdo:

S -> NP_sg VP_sg 
S -> NP_sg VP_pl 
NP_sg -> Kim 
NP_pl -> The cats 
VP_sg -> V_sg NP_sg 
VP_sg -> V_sg NP_pl 
V_sg -> sees 
V_pl -> see 
VP_pl -> V_pl NP_pl 
VP_pl -> V_pl NP_sg 

Aquí rechazaremos la sobregeneración de antes. Pero esto lleva a una explosión combinatoria muy rápidamente. Sin embargo podríamos aumentar cada término con una MAV y unificar juntos, cuando regrese de análisis:

S -> NP VP , C = A unified with B. 
NP -> kim /[ AGR sg ]. We mark Kim as being singular 
NP -> The cats/[ AGR pl ] 
VP[ AGR #1 ] -> V [ AGR #1 ] NP 

El # 1-notación están reentrancies, lo que significa que el valor de esta función debe ser la misma, de hecho ellos señalarán al mismo nodo en el gráfico después de la unificación, si es exitoso. Aquí en la práctica decimos que la característica de acuerdo de una frase verbal es la misma que la del verbo en la frase.

V -> See/[ AGR pl ] 
V -> Sees/[ AGR sg ] 

Con nuestra gramática aumentada juguete "Kim ver los gatos" es rechazado debido a que el NP y el vicepresidente no unificar, que tiene un valor diferente para su característica AGR. Cuando estamos analizando unificamos los AVM juntos, y por lo tanto ganamos mucha expresividad, lo que facilita a los ingenieros de gramática el escribir gramáticas. Por lo general, una UBG de cobertura amplia tiene en el orden de cien reglas, mientras que las CFG equivalentes, que pueden no existir, las CFG con unifacción están completas, tendrán reglas en el número de miles o más.

Para más detalles ver HPSG y LFG.

Answer 2

La programación lógica es, AFAIK, casi toda la unificación. Usted proporciona una declaración al intérprete, y el intérprete intenta unificarla con algo que sabe que es "verdadero", es decir, algo que está en su base de datos.

p. Ej.

cat(tom) :- true. 

Afirma que tom es un gato.

A continuación, puede consultar

?- cat(X). 

y prólogo volverá

X = tom 

Prolog busca en su base de datos y trata de unificar su estado de cuenta proporcionado (cat(X)) con un hecho que ya "sabe". En este caso, encuentra cat(tom) y por lo tanto puede decirle que X=tom.

Answer 3

Gracias a usted por estas respuestas detalladas. Ahora realmente lo entiendo Sin embargo, me gustaría escribir aquí un ejemplo que encontré en el libro "Inteligencia Artificial: Un Enfoque Moderno" de Stuart Russell y Peter Norvig en caso de que alguien esté buscando la misma pregunta nuevamente. Creo que esta respuesta utiliza un enfoque muy práctico:

reglas de inferencia Lifted requieren encontrar sustituciones que hacen diferentes expresiones lógicas parecen idénticos. Este proceso se llama unificación y es un componente clave de todos los algoritmos de inferencia de primer orden. El algoritmo UNIFY toma dos oraciones y devuelve un unificador para ellos si existe un .

Veamos algunos ejemplos de cómo debería comportarse UNIFY. Supongamos que tenemos una consulta Knows (John, x): ¿a quién conoce John ? Se pueden encontrar algunas respuestas a esta consulta al encontrar todas las oraciones en la base de conocimiento que se unifica con Knows (John, x). Aquí están los resultados de unificación con cuatro frases diferentes que podrían estar en la base conocimiento:

UNIFY(Knows(John, x), Knows(John, Jane)) = {x/Jane} 
UNIFY(Knows(John, x), Knows(y, Bill)) = {x/Bill, y/John} 
UNIFY(Knows(John, x), Knows(y, Mother(y))) = {y/John, x/Mother(John)} 
UNIFY(Knows(John, x), Knows(x, Elisabeth)) = fail 

La última unificación falla porque x no puede asumir los valores de John y Elizabeth en el Mismo tiempo.