1

2 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa: deducción versus inducción Deducción = razonamiento de lo general a lo específico –Preserva la verdad –Siempre es correcto Inducción = razonamiento desde lo específico a lo general el inverso de la deducción –No preserva la verdad –Puede haber evidencia estadística DEDUCCIÓN INDUCCIÓN Todos los hombres son mortales Sócrates es mortal Sócrates es un hombre Sócrates es mortal Todos los hombres son mortales

3 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa: inferencia y probabilidad Probabilidad de seleccionar un elemento de U siendo de P p(P)=|P| / |U| Dado un elemento seleccionado de U que es de Q, probabilidad de que sea de P p(P/Q)=p(P  Q) / p(Q) Teorema de Bayes: p(P/Q)=p(P) * p(Q/P) / p(Q) U P Q

4 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa: inferencia y probabilidad Interpretación probabilística del cálculo de predicados de primer orden (Carnap)  P representa el conjunto de modelos de Herbrand de la fórmula P (resp. Q) y U es 2 H(P  Q).  p(P)=p(P) son las interpretaciones de P que son modelo de P  p(P/Q) son los modelos de Q que son modelo de P p(False)=0p(True)=1 p(P  Q)= p(P  Q) p(P  Q)= p(P  Q) p(  P)=1- p(P)p(P)  p(Q) si P |= Q

5 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa: inferencia y probabilidad Dados B y E, hay más de una hipótesis candidata. –H = T = p(x 1,...,x n ) –H =  = E + Teorema de Bayes: Sea E una evidencia de T. Entonces p(T/E)=p(T) * p(E/T) / p(E)  Carnap: p(T) es la proporción de interpretaciones que son modelo de T  PARADOJA  Solomonoff: p(P)= 2 -  (P), donde  (P) es el contenido de información de la fórmula P (longitud en bits de la codificación mínima de P).

6 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa: inferencia y probabilidad  Teoría de la información de Shannon: I(P)=-log 2 p(P) –I(True) = 0 (p(True) = 1) –I(False) =  (p(False) = 0) –I(P  Q) = I(P) + I(Q) (p(P  Q) = p(P). p(Q))  Información de Bayes: I(T|E) = I (T) + I (E|T) - I (E)

7 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa: inferencia y probabilidad La teoría debe ser una explicación más simple que la propia evidencia I(T|E)  I(B  E) T comprime los ejemplos al tener menor contenido de información. p(T/E)=p(T) * p(E/T) / p(E)  1 p(T) * p(E/T)  p(E)  0  I(E)  I(T) + I(E/T)  I(T|E)  I(T) + I(E/T)  I(B  E) 0

8 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa: inferencia y probabilidad Principio de la longitud de descripción mínima de Rissanen: minimizar I(T|E) Principio de la navaja de Ockham: minimizar I(T) Principio de la probabilidad máxima de Fisher: maximizar I(E|T) TEOREMA DE EQUIVALENCIA: Sea E una evidencia para un conjunto de teorías (potenciales) elegidas desde . min T  I(T|E) = - log 2 max T  p(T|E)

9 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa Búsqueda en el espacio de las hipótesis –estados: hipótesis de L H –objetivo: encontrar una hipótesis que satisfaga el criterio de calidad (ej. completitud y consistencia) Algoritmo de generación y prueba para todo H  L H hacer si H es completa y consistente entonces output(H)  computacionalmente caro Restringir la búsqueda –lenguaje: reducir el espacio de hipótesis –búsqueda: reducir la búsqueda en el espacio de las hipótesis

10 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa Estructura del espacio de hipótesis basado en una relación de generalidad G es más general que S iff covers(S)  covers(G) Podando el espacio de búsqueda –Si H no cubre un ejemplo e entonces tampoco cubrirá ninguna especialización de e  usado con los ejemplos positivos para podar –Si H cubre un ejemplo e entonces también cubrirá sus generalizaciones  usado con los ejemplos negativos para podar Estas propiedades determinan el espacio de las soluciones posibles

11 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa: espacio de hipótesis - + + + + - - - - muy general muy específico ¿Cómo estructurar el espacio de las hipótesis? ¿Cómo movernos desde una hipótesis a otra?

12 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa: espacio de hipótesis Más general Más específico

13 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa: espacio de hipótesis Más general Más específico e- cubierto    e- no cubierto

14 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa: espacio de hipótesis Más general Más específico flies(X)  flies(X)  bird(X) flies(X)  bird(X), normal(X)

15 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa: espacio de hipótesis Más general Más específico flies(X)  flies(X)  bird(X) flies(X)  bird(X), normal(X)  flies(oliver)  bird(oliver)

16 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa: noción de generalidad Noción de generalidad –¿Cómo especializar las condiciones? –¿Cómo generalizar las condiciones?

17 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa: noción de generalidad El conjunto de los términos de primer orden es un retículo –t 1 es más general que t 2 iff para alguna sustitución  : t 1  = t 2 –especialización: aplicar una sustitución –generalización: aplicar una sustitución inversa g(f(X),Y) g(f(X),X)g(f(f(a)),X)g(f(X),f(a)) g(f(f(a)),f(a))

18 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa: noción de generalidad El conjunto de las cláusulas es un retículo –C 1 es más general que C 2 iff para alguna sustitución  : C 1   C 2 –especialización: aplicar una sustitución y/o añadir un literal –generalización: aplicar una sustitución inversa y/o eliminar un literal m(X,Y) m(X,X) m(X,[Y|Z]) m([X|Y],Z)m(X,Y):-m(Y,X) m(X,[X|Z])m(X,[Y|Z]):-m(X,Z)

19 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa: noción de generalidad Una teoría G es más general que una teoría S iff G  = S –G  = S: en cada interpretación en la que G es cierto, S también lo es –“G implica lógicamente S” Todas las frutas saben bien  = Todas las manzanas saben bien (asumiendo que las manzanas son frutas)

20 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa: deducción versus inducción Hay operadores deductivos  - que implementan (o aproximan)  = resolución Invertir estos operadores conduce a operadores inductivos Técnica básica en muchos sistemas de programación lógica inductiva

21 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 2. Búsqueda de cláusulas del programa: varios marcos para la generalidad Dependiendo de la forma de G y S –1 cláusula / cjto de cláusulas / cualquier teoría de primer orden Dependiendo en el mecanismo deductivo  - a invertir –Theta-subsunción –Resolución –Implicación

22 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: theta- subsunción (Plotkin) Subsunción –Sustitución:  = {X 1 /t 1,...,X n /t n } es una asignación de los términos t i a las variables X i –Subsunción: Sean C y D cláusulas. C (  -)subsume D (C =  D) iff existe  tal que C   D Ejemplo: p(a,b)  r(b,a) es subsumida por p(X,Y)  r(Y,X) p(X,Y)  r(Y,X) subsume p(X,Y)  r(Y,X),q(X)

23 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: theta- subsunción (Plotkin) Ejercicio: C1: father(X,Y)  parent(X,Y). C2: father(X,Y)  parent(X,Y),male(X). C3: father(luc,Y)  parent(luc,Y). C1 =  C2(  ={ }) C1 =  C3(  ={ X/luc }) C2 =/  C3 C3 =/  C2

24 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: theta- subsunción (Plotkin) Ejercicio: C1: p(X,Y)  q(X,Y). C2: p(X,Y)  q(X,Y),q(Y,X). C3: p(Z,Z)  q(Z,Z). C4: p(a,a)  q(a,a). C1 =  C2(  ={ }) C1 =  C3(  ={ X/Z,Y/Z }) C1 =  C4(  ={ X/a,Y/a }) C3 =  C4(  ={ Z/a })

25 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: theta- subsunción (Plotkin) Ejercicio: C1: p(f(X),g(X))  C2: p(f(3),g(3))  Ejercicio: C1: p(f(X),g(X))  C2: p(f(3),g(Y))  C1 =  C2(  ={ X/3 }) C1 =/  C2 C2 =/  C1

26 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: theta- subsunción (Plotkin) Propiedades de la  -subsunción –Correcta: si C = < D entonces C |= D –Incompleta: puede que C |= D y sin embargo C =/ < D C: p(f(X))  p(X) D: p(f(f(X)))  p(X) –Reflexiva, transitiva y antisimétrica  relación de semi-orden clases de equivalencia con un orden parcial c1  c2 sii c1 = < c2 y c2 = < c1 Si c  [C] y d  [D]  c = < d ó d = < c ó (c =/ < d y d =/ < c)

27 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: theta- subsunción (Plotkin) Las clases de equivalencia forman un retículo p(X,Y) :- m(X,Y),r(X) p(X,Y) :- m(X,Y), m(X,Z),r(X)... p(X,Y) :- m(X,Y),s(X) p(X,Y) :- m(X,Y), m(X,Z),s(X)... p(X,Y) :- m(X,Y) p(X,Y) :- m(X,Y), m(X,Z) p(X,Y) :- m(X,Y),m(X,Z),m(X,U)... p(X,Y) :- m(X,Y),s(X),r(X) p(X,Y) :- m(X,Y), m(X,Z),s(X),r(X)... lgg glb

28 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: generalización menos general - lgg (Plotkin) Generalización menos general (lgg) C es la generalización menos general (lgg) de D bajo  -subsunción si C =  D y para cada E tal que E =  D se cumple E =  C. Computación de lgg Cuando nos restringimos a átomos con el mismo signo y el mismo símbolo de predicado (compatibles) la lgg es el dual de la unificación  lgg(f 1 (l 1,...,l n ),f 2 (m 1,...,m n ) = vsi f 1  f 2 = f 1 (lgg(l 1,m 1 ),...,lgg(l n,m n ))si f 1 = f 2

29 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: generalización menos general - lgg (Plotkin) Ejemplo: l = member(3,cons(2,cons(3,nil))) l’ = member(3,cons(4,cons(5,cons(6,nil)))) m = member(3,cons(v 2,4,cons(v 3,5,v nil,cons(6,nil) ))) m = member(3,cons(x,cons(y,z)))

30 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: generalización menos general - lgg (Plotkin) Ejercicio l: p(f(5,3),g(2,3)) l’: p(f(1,2),g(3,2)) l’’: p(f(1,4),g(5,4)) lgg = p(f(X,W),g(Y,Z))

31 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: generalización menos general - lgg (Plotkin)  Sean C y D dos cláusulas. El lgg de C y D en el orden de subsunción es lgg(C,D)=  lgg(l,m) | l  C y m  D y l y m son compatibles} Dadas dos cláusulas, el lgg es la cláusula simple más específica que es mas general que ambas. Ejemplo: f(t,a)  p(t,a), m(t),f(a) f(j,p)  p(j,p), m(j),m(p) lgg = f(X,Y)  p(X,Y),m(X),m(Z)

32 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: generalización menos general - lgg (Plotkin) Ejemplo rev([2,1],[3],[1,2,3])  rev([1],[2,3],[1,2,3]) rev([a],[ ],[a])  rev([ ],[a],[a]) Ejercicio a([1,2],[3,4],[1,2,3,4])  a([2],[3,4],[2,3,4]) a([a],[ ],[a])  a([ ],[ ],[ ]) lgg = rev([A,B],C,[D|E])  rev(B,[A|C]),[D|E]) A B C D E B A C D E lgg = a([A|B],C,[A|D])  a(B,C,D)

33 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: generalización menos general - lgg (Plotkin) Ejercicio m(c,[a,b,c])  m(c,[b,c]), m(c,[c]) m([a],[a,b])  m(a,[a]) lgg = m(P,[a,b|Q])  m(P,[R|Q]),m(P,[P])

34 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: generalización menos general relativa- rlgg (Plotkin) Generalización menos general relativa (rlgg) –relativa a la teoría de conocimiento B –rlgg(e1,e2)=lgg(e1  B,e2  B) Ejemplo: C1: uncle(X,Y):-brother(X,father(Y)). C2: uncle(X,Y):-brother(X,mother(Y)). B: parent(father(X),X). parent(mother(X),X). lgg(C1,C2) = uncle(X,Y):-brother(X,Z). rlgg(C1,C2) = uncle(X,Y):-brother(X,U),parent(U,Y).

35 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: generalización menos general relativa- rlgg (Plotkin)  Una cláusula C es más general que D con respecto a una teoría T si T  C |- D.  Un átomo A es una lgg de un átomo B con respecto a una teoría T si existe un unificador  tal que T |- A   B (A=  T B).  Una cláusula C es una lgg de una cláusula D con respecto a una teoría T (rlgg) si T |- C   D para alguna sustitución .

36 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: generalización menos general relativa- rlgg (Plotkin)  Problema: no siempre existe rlgg de un conjunto de cláusulas con respecto a una teoría. –C1: q(f(a)). C2: q(g(a)). –B: p(f(X),Y). p(g(X),Y). –C : q(X):-p(X,g 1 (X)),…,p(X,g n (X)) es una generalización  Excepción: rlgg existe siempre si T es básica (GOLEM).

37 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: generalización de Buntine  rlgg puede conducir a conclusiones contraintuitivas. EJEMPLO: –C: pequeño(X):-gato(X). D: muñeco_mascota(X):- de_peluche(X), gato(X). –P: mascota(X):- gato(X). muñeco_mascota(X):-pequeño(X),de_peluche(X),mascota (X). C =  P D Si asumimos que una cláusula C es más general que otra D si cualquier interpretación de C permite obtener las mismas conclusiones que con D. En el ejemplo anterior C no es más general que D.

38 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: generalización de Buntine  Subsunción generalizada (cláusulas definidas) Una cláusula C es más general que otra D w.r.t. un programa P C =  B P D si para cualquier interpretación de Herbrand I modelo de P, entonces T D (I)  T C (I). En el ejemplo anterior C y D no pueden compararse ya que tienen distintas cabezas.

39 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: generalización de Buntine  Visión operacional Sean C y D cláusulas con variables disjuntas y sea P un programa lógico. Sea  una sustitución que asigna a las variables de D nuevas constantes (que no aparecen en C,D ni P).Entonces, C =  B P D sii existe una sustitución  tal que: C head  = D head  P  D body   (C body  )

40 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: generalización de Buntine  Procedimiento: C es más general que D wrt P si C puede convertirse en D aplicando repetidamente:  Transformar las variables en constantes o en otros términos  Añadir átomos al cuerpo  Evaluar parcialmente el cuerpo resolviendo cláusulas en P contra un átomo del cuerpo.

41 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: generalización de Buntine  Subsunción generalizada versus generalización de Plotkin. C =  B  D sii C =  D  Subsunción generalizada versus generalización menos general relativa. C =  B P D sii C aparece en la raíz de una refutación en la demostración de P  (C  D) =  B P un caso especial de rlgg

42 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: resolución inversa Resolución C 1 C 2  1  2 C RESOLUCIÓN: C = C 1  C 2  l 1  C 1  l 2  C 2 | C 1 y C 2 variables disjuntas   = mgu(l 1, l 2 ) s.t. l 1  = l 2 ,  =  1  2  l 1  1 = l 2  2 C=(C 1 -  l 1  )  1  (C 2 -  l 2  )  2

43 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: resolución inversa Ejemplo: –p(X)  q(X ) y q(X)  r(X,Y) conduce a p(X)  r(X,Y) –p(X)  q(X ) y q(a) conduce a p(a)  Inversión de la resolución: obtención de C 1 (o C 2 ) a partir de C y C 2 (C 1 ). No hay una solución única EJEMPLO: C 2 = B  E,F C = A  E,F,C,D C 1 = A  B,C,D C 1 ’ = A  B,C,D,E C 1 ’’ = A  B,C,D,F C 1 ’’’ = A  B,C,D,E,F

44 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: resolución inversa  El problema es aún más agudo para cláusulas de primer orden EJEMPLO: C 1 =  mas_pesado(martillo,pluma) C =  mas_denso(martillo,pluma),mas_grande(martillo,pluma) C 2 = mas_pesado(martillo,pluma)  mas_denso(martillo,pluma), mas_grande(martillo,pluma) C’ 2 = mas_pesado(A,B)  mas_denso(A,B), mas_grande(A,B) Para generar C 2 debemos decidir qué términos se convierten en variables y cómo

45 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: resolución inversa El operador V C 1 C 2  1  2 C OPERADOR V: Produce C 2 a partir de C y C 1 dadas dos cláusulas C 1 y C, el V-operador encuentra C 2 tal que C es una instancia de un resolvente de C 1 y C 2. Generaliza  C 1,C} a  C 1, C 2 }

46 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: resolución inversa Absorción –desde q  A y p  A,B –inferir p  q,B Identificación –desde p  q,B y p  A,B –inferir q  A p  q,Bq  A p  A,B p  q,Bq  A p  A,B

47 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: resolución inversa Absorción: el cuerpo de C 1 es absorbido en el cuerpo de C (después de una unificación) y reemplazado por su cabeza EJEMPLO: C: pajaro(tweety):-tiene_plumas(tweety), tiene_alas(tweety),tiene_pico(tweety). C 1 : vuela(X):- tiene_plumas(X),tiene_alas(X).  =  X/tweety } C 2 : pajaro(tweety):-vuela(tweety), tiene_pico(tweety).

48 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: resolución inversa Ejemplo: P={ animal(tiburon) nadar(tiburon) } e={ pez(tiburon) } Encontrar dos cláusulas que tengan un resolvente del que pez(tiburon) es una instancia –Cláusula de entrada: una cláusula de P ( nadar(tiburon) ) –Cláusula central: Por ejemplo, la menos general ( pez(tiburon)  nadar(tiburon) ) P |/=e

49 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: resolución inversa –Cláusula de entrada: una cláusula de P ( animal(tiburon) ) –Cláusula central: Por ejemplo, la menos general ( pez(X)  animal)X),nadar(X) ). pez(x)  animal(x), nadar(x) animal(tiburon) pez(tiburon)  nadar(tiburon) nadar(tiburon) pez(tiburon)

50 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: resolución inversa Identificación: identificar parte del cuerpo de C 2 en el cuerpo de C a través de una sustitución . Encontrar un literal l en el cuerpo de C 2 que no ocurre en el de C. La identificación construye C 1 con cabeza l y cuerpo la parte de C que no está en C 2. EJEMPLO: C: pajaro(tweety):-tiene_plumas(tweety), tiene_alas(tweety),tiene_pico(tweety). C 2 : pajaro(tweety):- vuela(tweety),tiene_pico(tweety). l: vuela(tweety) C-C 2 : { tiene_plumas(tweety), tiene_alas(tweety) } C 1 : vuela(tweety):- tiene_plumas(tweety), tiene_alas(tweety).

51 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: resolución inversa El operador W C 1 A C 2  C1  A,1  A,2  C2 B 1 B 2 OPERADOR W Dadas dos cláusulas  B 1,B 2 } encontrar  C 1,A,C 2 } tal que B 1 es una instancia de un resolvente de C 1 y A, y B 2 es una instancia de un resolvente de A y C 2. Generaliza  B 1, B 2 } a  C 1, A,C 2 }

52 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: resolución inversa Intra-construcción –desde p  A,B y p  A,C –inferir q  B y p  A,q y q  C Inter-construcción –desde p  A,B y q  A,C –inferir p  r,B y r  A,q y q  r,C p  r,B r  A q  r,C p  A,B q  A,C q  B p  A,q q  C p  A,B p  A,C

53 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: resolución inversa Cuando l no está ni en B 1 ni en B 2, el operador W se inventa predicados.

54 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: implicación inversa Sean dos cláusulas C y D. decimos que C implica D (C  D) iff cada modelo de C es modelo de D (C  D). C es una generalización bajo implicación de D.  la generalización bajo  –subsunción es incompleta. C  D y C =/  D  Inversión implicación es una forma completa de generalización.  indecidible  computacionalmente caro  cláusulas recursivas

55 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: implicación inversa  Diferencia entre implicación y  –subsunción: cláusulas ambivalentes.  Una cláusula es ambivalente sii contiene un par (C,  D) de literales ambivalentes, es decir, C y D tienen el mismo símbolo de predicado y signo. p(X):-p(X). q(a):-q(s(s(a))). Sean C y D no ambivalentes. Entonces, C  D sii C =  D.

56 Diciembre 2001Fundamentos Lógicos de la Ingeniería del Software 3. Métodos Bottom-up: implicación inversa RELACIÓN ENTRE IMPLICACIÓN Y RESOLUCIÓN C  D  D es una tautología  C =  D  E =  D y E se obtiene resolviendo C consigo misma.