Unificación

Unificación

Unificación: La unificación es un proceso que permite, mediante la sustitución de variables por términos, obtener, a partir de un par de fórmulas, una tercera que será verdadera siempre que cualquiera de las primeras lo sea. Esta característica hace de la unificación una herramienta muy útil en la demostración formal de teoremas. Veamos los fundamentos necesarios para poder llevar a cabo este proceso.

Sustitución

El primer concepto relacionado con la unificación es el de sustitución:
definición. Se llama sustitución a un conjunto finito de la forma {t1/v1,…,tn/vn}, donde cada vi es una variable, cada ti es un término dis­tinto de vi y para 1 < i, j < n, i ǂ j, vi ǂ vj.
Son ejemplos de sustituciones:
1.{a/x, f(b)/y}
2.{y/x, b/z}
3.{b/x, b/y, f(a)/z}
No son sustituciones:
1.{a/x, b/x}; la variable x aparece sustituida por dos términos distintos
2.{a/x, y/y, f(a)/z}; la variable y aparece sustituida por ella misma.
3.{a/b, y/y, f(a)/z}; b no puede ser sustituida pues no es una variable.
La utilidad de las sustituciones es que se puede obtener, a partir de una sustitución y una fórmula, una nueva fórmula que será verdadera siempre que la primera lo sea, a esto se la llama aplicar la sustitución a la fórmula y se denota Fσ, donde F es la fórmula y σ la sustitución. El procedimiento para obtener Fσ es muy simple y consiste en sustituir en F, todas las ocurrecias de variables que aparezcan en σ, por el término que le corresponda en la propia σ.
El siguiente ejemplo ilustra como aplicar una sustitución a una fórmula:
Sean F = A(x, f(y), g(z)) y σ = {a/z, f(b)/x}.
Para obtener Fσ se analizan las variables de F, en primer lugar aparece x, como x está sustituida en σ por f(b), se procede a sustituirla en F, obteniéndose:
A(f(b), f(y), g(z))
Si x tuviera otras ocurrencias en F, debería ser sustituida en todas por f(b), pero como no es el caso, se procede directamente a analizar la próxima variable de F. La variable y no aparece sustituida en σ por lo que se deja intacta en F, pasándose al análisis de la última variable, z, la que aparece en σ
sustituida por a, lo que hace que finalmente quede:
Fσ = A(f(b), f(y), g(a))

Composición de sustituciones

Dos sustituciones pueden componerse para obtener una nueva. Si σ y σ' son sustituciones, la composición de σ y σ' se denota como σσ' y es el resultado de aplicar σ' a todos los términos de σ, adicionar al conjunto resultante todos los elementos de σ' cuyas variables no se encuentren entre las variables de σ y finalmente eliminar todos los elementos ti/vi que cumplan que ti = vi.
El siguiente ejemplo ilustra como componer sustituciones:
Sean σ = {v/x, w/y, f(a)/z} y σ' = {y/w, a/v, b/z, f(b)/u}
Para obtener σσ' el primer paso es aplicar σ' a todos los términos de σ, que en este caso son v, w y f(a). Como resultado se obtiene {a/x, y/y, f(a)/z}.
El segundo paso es adicionar y/w, a/v y f(b)/u al conjunto pues w, v y u no aparecen entre las variables de σ, resultando {a/x, y/y, f(a)/z, y/w, a/v, f(b)/u}
Finalmente se elimina y/y por lo que se obtiene:
σσ' = {a/x, f(a)/z, y/w, a/v, f(b)/u}

Unificador y unificador más general

Existen parejas de fórmulas a partir de las que se puede obtener, aplicando determinada sustitución a ambas, el mismo resultado. En tales casos se dice que las fórmulas son unificables y a la sustitución se le llama unificador. A continuación se presentan dos parejas de fórmulas unificables y sus respectivos unificadores:
1.F1a = Q(x, b) F1b = Q(a, y) σ = {a/x, b/y}
F1aσ = F1bσ = Q(a, b)
2.F2a = R(f(y), x) F2b = R(z, f(a)) σ = {f(y)/z, f(a)/x}
F2aσ = F2bσ = R(f(y), f(a))
La utilidad de los unificadores en la demostración de teoremas, radica en que la fórmula obtenida al aplicar el unificador a una pareja unificable es consecuencia lógica de ambas fórmulas de la pareja. En otras palabras, es verdadera siempre que cualquiera de estas lo es, o más útil aún, si es falsa, puede afirmarse que las originales lo son también, lo que es utilizado en la demostración por refutación, que se estudiará más adelante.
Cuando una pareja de fórmulas es unificable, es posible encontrar un conjunto infinito de unificadores, unos mucho más simples que otros. Por supuesto que, al utilizar un unificador, es muy conveniente que sea el más simple posible, a este se le llama unificador más general (UMG) y se define como:
definición. Si A y B son fórmulas, se dice que γ es el UMG de A y B si para todo σ, unificador de A y B, existe una sustitución σ' tal que Aσ=Aγσ'

Algoritmo de unificación de Robinson

La definición de UMG no establece directamente el modo de encontrarlo, que es lo que realmente se necesita. A continuación se presenta un método, conocido como el algoritmo de unificación de Robinson, que dadas dos fórmulas A y B, permite determinar si son unificables y en tal caso encontrar su UMG.
Antes de describir el algoritmo, es preciso introducir una definición:
definición. Sean A y B fórmulas, se denomina conjunto desacuerdo (D) al conjunto formado por los dos primeros términos en los cuales difieren A y B.
Ejemplos:
1.A = P(x, f(y)) B = P(x, f(y)) D = {}
2.A = P(x, f(y)) B = P(z, f(a)) D = {x, z}
3.A = R(x, f(a)) B = R(g(a), g(y)) D = {x, g(a)}
4.A = P(a, g(y)) B = P(a, f(a)) D = {g(y), f(a)}
5.A = P(f(a), g(y)) B = P(f(x), f(a)) D = {a, x}
Es importante tener en cuenta la diferencia que existe entre situaciones del tipo presente en el ejemplo 4, y del tipo presente en el 5. En el primer caso, la diferencia está en los símbolos de función (f y g), por lo que en D están ambos símbolos con sus respectivos argumentos, sin embargo, en el segundo caso los símbolos de función son idénticos, estando la diferencia en los argumentos (a y x).
Algoritmo de unificación de Robinson:
Entrada: A y B fórmulas.
1.- k= 0, σ0 = {}
2.- Si Aσk = Bσ'k, entonces fin: UMG = σk.
en otro caso Hallar Dk, conjunto desacuerdo de Aσk y Bσk.
3.-Si hay en Dk una variable (v) y un término (t) tales que v no ocurre en t,
entonces:
σk+1 = σk {t/v},
k = k+1,
ir a paso 2.
En caso contrario fin: A y B no son unificables.
Puede decirse que el algoritmo consiste en ir construyendo iterativamente, a partir del conjunto desacuerdo, el UMG.
En cada iteración se aplica, a ambas fórmulas, la sustitución construida hasta ese momento, si se obtiene el mismo resultado, ya se encontró el UMG. De lo contrario, se busca el conjunto desacuerdo, pero no de A y B, sino del resultado de aplicar la sustitución a cada uno. Este último detalle es muy importante, pues de no tenerse en cuenta, siempre se obtendría el mismo conjunto desacuerdo y el algoritmo no terminaría.
Una vez calculado el conjunto desacuerdo (D), se examina en busca de una variable (v) y un término (t) donde no ocurra v, donde pueden darse las siguientes situaciones:
1.D = {v1, v2}, donde v1 ǂ v2 y ambas son variables. Se puede tomar una cualquiera como v y la otra como t (por supuesto, las variables también son términos).
2.D = {v', t'}, donde v' es una variable y t' una constante o función que no tiene como argumento a v'. Se toma a v' como v y t' como t.
3.D = {v', t'(v')}, donde v' es una variable y t' una función que tiene como argumento a v'. No son unificables A y B.
4.D = {t₁, t₂}, donde ni t₁, ni t₂ son variables. No son unificables A y B.
Si se encontraron v y t, entonces se construye la nueva sustitución como la composición de la anterior con {t/v} y se va una nueva iteración.
A continuación se presenta dos ejemplos donde se aplica el algoritmo a un par de fórmulas, en el primer caso unificables y el segundo no:
Primer caso.
A = R(x, f(a)) B = R(b, z)
Primera iteración.
k = 0 σ0 = {}
Aσ0 = A Bσ0 = B Aσ0 ǂ Bσ0
D0 = {x, b} v = x t = b
Segunda iteración.
k = 1 σ1 = {}{b/x} = {b/x}
Aσ1 = R(b, f(a)) Bσ1 = R(b, z) Aσ1 ǂ Bσ1
D0 = {f(a), z} v = z t = f(a)
Tercera iteración.

k = 2 σ2 = {b/x}{f(a)/z} = {b/x, f(a)/z}
Aσ2 = R(b, f(a)) Bσ2 = R(b, f(a)) Aσ2 = Bσ2
El UMG es {b/x, f(a)/z}
Segundo caso.
A = R(x, f(x)) B = R(z, z)
Primera iteración.
k = 0 σ0 = {}
Aσ0 = A Bσ0 = B Aσ0 ǂ Bσ0
D0 = {x, z} v = x t = z
Segunda iteración.
k = 1 σ1 = {}{z/x} = {z/x}
Aσ1 = R(z, f(z)) Bσ1 = R(z, z) Aσ1 ǂ Bσ1
D0 = {f(z), z} la variable ocurre en el término, A y B no son unificables.

Enlaces externos

http://www.monografias.com/trabajos15/logica-metodologia/logica-metodologia.shtml?monosearch

http://www.euclides.org/menu/articles/article101.htm

Bibliografía

Brito, M. L. y B. Deiros (2000). La enseñanza de la matemática y la globalización. Evento INFOMADI. Cuba

Calderón, R. M. (1999), La enseñanza del Cálculo Integral. Experiencia en Ingeniería Mecánica. Revista de la Universidad Autónoma "Gabriel René Moreno". Bolivia.

Calderón, R. M. y E. Fraga (2000). La Evaluación en Matemáticas: Valoraciones y Alternativas. En Memorias del Evento Internacional INFOMADI, La Habana, Ministerio de Educación Superior, Cuba.

Carlos Rodríguez, E. (2000). La superación del profesor de matemática en la Universidad de hoy. Una experiencia cubana. Acta Latinoamericana de Matemática Educativa. Vol. XIII.

Colectivo de autores (1995). Métodos participativos. ¿Una nueva concepción de la enseñanza?. CEPES-UH.

Colectivo de autores, (1998). Sistema didáctico para la introducción de la computación en la disciplina Matemática en las carreras de ingeniería mecánica y metalúrgica. ISPJAE. Cuba.

Chávez J. (1998). Actualidad de las tendencias educativas. Cuba

De Guzmán M. (1994). Programas de ordenador en la educación matemática. En Revista Anaya Educación, 3 (34-40) España.

Deiros Fraga B. y Calderón R. M. (2001). La matemática para ingeniería: algunas propuestas metodológicas. Ponencia presentada al Primer Congreso Iberoamericano de docentes de ingeniería y afines. Ciudad de La Habana.

Díaz Barriga, F. y G. Hernández (1998). Estrategias docentes para un aprendizaje significativo. Una interpretación constructivista. Mc Graw Hill.

González, O. (1990). Perfeccionamiento de la enseñanza de las disciplinas y la formación de habilidades y capacidades específicas. Informe Final, La Habana.

Hernández, H. y otros (1997), Cuestiones de Didáctica de la Matemática. Conceptos y Procedimientos en la Educación Polimodal y Superior, Homo Sapiens Ediciones, Argentina.

Hernández, H.: El perfeccionamiento de la enseñanza de la Matemática en la Educación Superior Cubana. Experiencia en Algebra Lineal. Tesis de Doctorado, MES.1989.

Hernández, L. (2001). Una vía transdisciplinar sobre las NTIC para el desarrollo de habilidades profesionales generales, en cursos de posgrado semipresenciales Tesis de Doctorado". Cuba.

NCTM. Estándares curriculares y de evaluación para la Educación Matemática. SAEM Thales.

Rodríguez, T. (1991). Enfoque sistémico en la dirección de la asimilación de los conceptos básicos de la Disciplina Matemática Superior. Tesis de Doctorado.