Source: https://www.slideshare.net/JoseAAlonso/li2011t11-resolucin-en-lgica-de-primer-orden
Timestamp: 2017-03-24 12:44:31+00:00

Document:
LI-T6: Sintaxis y semántica de la l...
DAO2011-T0: Presentación de sistema...
LI2011-T8: Tableros semánticos para...
Se presentan los algoritmos de unificación y resolución en lógica de primer orden.
Este es el tema 11 del curso de "Lógica informática". Más temas en http://www.cs.us.es/~jalonso/cursos/li/tema
at UAM CUAJIMALPA
PD Tema 11: Resolución en lógica de primer orden Lógica informática (2010–11) Tema 11: Resolución en lógica de primer orden José A. Alonso Jiménez Andrés Cordón Franco María J. Hidalgo Doblado Grupo de Lógica Computacional Departamento de Ciencias de la Computación e I.A. Universidad de Sevilla 1 / 31 2.
PD Tema 11: Resolución en lógica de primer ordenTema 11: Resolución en lógica de primer orden 1. Introducción 2. Uniﬁcación 3. Resolución de primer orden 2 / 31 3.
PD Tema 11: Resolución en lógica de primer orden IntroducciónTema 11: Resolución en lógica de primer orden 1. Introducción Ejemplos de consecuencia mediante resolución 2. Uniﬁcación 3. Resolución de primer orden 3 / 31 4.
PD Tema 11: Resolución en lógica de primer orden Introducción Ejemplos de consecuencia mediante resoluciónEjemplos de consecuencia mediante resolución Ejemplo 1: {∀x [P(x ) → Q(x )], ∃x P(x )} |= ∃x Q(x ) se reduce a {{¬P(x ), Q(x )}, {P(a)}, {¬Q(z)}} es inconsistente. Demostración: 1 {¬P(x ), Q(x )} Hipótesis 2 {P(a)} Hipótesis 3 {¬Q(z)} Hipótesis 4 {Q(a)} Resolvente de 1 y 2 con σ = [x /a] 5 Resolvente de 3 y 4 con σ = [z/a] 4 / 31 5.
PD Tema 11: Resolución en lógica de primer orden Introducción Ejemplos de consecuencia mediante resoluciónEjemplos de consecuencia mediante resolución Ejemplo 2: {∀x [P(x ) → Q(x )], ∀x [Q(x ) → R(x )]} |= ∀x [P(x ) → R(x )] se reduce a {{¬P(x ), Q(x )}, {¬Q(y ), R(y )}, {P(a)}, {¬R(a)}} es inconsistente. Demostración: 1 {¬P(x ), Q(x )} Hipótesis 2 {¬Q(y ), R(y )} Hipótesis 3 {P(a)} Hipótesis 4 {¬R(a)} Hipótesis 5 {Q(a)} Resolvente de 1 y 3 con σ = [x /a] 6 {R(a)} Resolvente de 2 y 5 con σ = [y /a] 5 Resolvente de 4 y 6 con σ = 5 / 31 6.
PD Tema 11: Resolución en lógica de primer orden UniﬁcaciónTema 11: Resolución en lógica de primer orden 1. Introducción 2. Uniﬁcación Uniﬁcadores Composición de sustituciones Comparación de sustituciones Uniﬁcador de máxima generalidad Algoritmo de uniﬁcación 3. Resolución de primer orden 6 / 31 7.
PD Tema 11: Resolución en lógica de primer orden Uniﬁcación UniﬁcadoresUniﬁcadores Def.: La sustitución σ es un uniﬁcador de los términos t1 y t2 si t1 σ = t2 σ. Def.: Los términos t1 y t2 son uniﬁcables si tienen algún uniﬁcador. Def.: t es una instancia común de t1 y t2 si existe una sustitución σ tal que t = t1 σ = t2 σ. Ejemplos: t1 t2 Uniﬁcador Instancia común f (x , g(z)) f (g(y ), x ) [x /g(z), y /z] f (g(z), g(z)) f (x , g(z)) f (g(y ), x ) [x /g(y ), z/y ] f (g(y ), g(y )) f (x , g(z)) f (g(y ), x ) [x /g(a), y /a] f (g(a), g(a)) f (x , y ) f (y , x ) [x /a, y /a] f (a, a) f (x , y ) f (y , x ) [y /x ] f (x , x ) f (x , y ) g(a, b) No tiene No tiene f (x , x ) f (a, b) No tiene No tiene f (x ) f (g(x )) No tiene No tiene Nota: Las anteriores deﬁniciones se extienden a conjuntos de términos y de literales. 7 / 31 8.
PD Tema 11: Resolución en lógica de primer orden Uniﬁcación Composición de sustitucionesComposición de sustituciones e identidad Composición de sustituciones: Def.: La composición de las sustituciones σ1 y σ2 es la sustitución σ1 σ2 deﬁnida por x (σ1 σ2 ) = (x σ1 )σ2 , para toda variable x . Ejemplo: Si σ1 = [x /f (z, a), y /w ] y σ2 = [x /b, z/g(w )], entonces – x σ1 σ2 = (x σ1 )σ2 = f (z, a)σ2 = f (zσ2 , aσ2 ) = f (g(w ), a) – y σ1 σ2 = (y σ1 )σ2 = w σ2 = w – zσ1 σ2 = (zσ1 )σ2 = zσ2 = g(w ) – w σ1 σ2 = (w σ1 )σ2 = w σ2 = w Por tanto, σ1 σ2 = [x /f (g(w ), a), y /w , z/g(w )]. Def.: La substitución identidad es la sustitución tal que, para todo x , x = x . Propiedades: 1. Asociativa: σ1 (σ2 σ3 ) = (σ1 σ2 )σ3 2. Neutro: σ = σ = σ. 8 / 31 9.
PD Tema 11: Resolución en lógica de primer orden Uniﬁcación Comparación de sustitucionesComparación de sustituciones Def.: La sustitución σ1 es más general que la σ2 si existe una sustitución σ3 tal que σ2 = σ1 σ3 . Se representa por σ2 ≤ σ1 . Def.: Las sustituciones σ1 y σ2 son equivalentes si σ1 ≤ σ2 y σ2 ≤ σ1 . Se representa por σ1 ≡ σ2 . Ejemplos: Sean σ1 = [x /g(z), y /z], σ2 = [x /g(y ), z/y ] y σ3 = [x /g(a), y /a]. Entonces, 1. σ1 = σ2 [y /z] 2. σ2 = σ1 [z/y ] 3. σ3 = σ1 [z/a] 4. σ1 ≡ σ2 5. σ3 ≤ σ1 Ejemplo: [x /a, y /a] ≤ [y /x ], ya que [x /a, y /a] = [y /x ][x /a, y /a]. 9 / 31 10.
PD Tema 11: Resolución en lógica de primer orden Uniﬁcación Uniﬁcador de máxima generalidadUniﬁcador de máxima generalidad Def.: La sustitución σ es un uniﬁcador de máxima generalidad (UMG) de los términos t1 y t2 si – σ es un uniﬁcador de t1 y t2 . – σ es más general que cualquier uniﬁcador de t1 y t2 . Ejemplos: 1. [x /g(z), y /z] es un UMG de f (x , g(z)) y f (g(y ), x ). 2. [x /g(y ), z/y ] es un UMG de f (x , g(z)) y f (g(y ), x ). 3. [x /g(a), y /a] no es un UMG de f (x , g(z)) y f (g(y ), x ). Nota: Las anterior deﬁnición se extienden a conjuntos de términos y de literales. 10 / 31 11.
PD Tema 11: Resolución en lógica de primer orden Uniﬁcación Algoritmo de uniﬁcaciónUniﬁcación de listas de términos Notación de lista: (a1 , . . . , an ) representa una lista cuyos elementos son a1 , . . . , an . (a|R) representa una lista cuyo primer elemento es a y resto es R. () representa la lista vacía. Uniﬁcadores de listas de términos: Def.: σ es un uniﬁcador de (s1 . . . , sn ) y (t1 . . . , tn ) si s1 σ = t1 σ, . . . , sn σ = tn σ. Def.: (s1 . . . , sn ) y (t1 . . . , tn ) son uniﬁcables si tienen algún uniﬁcador. Def.: σ es un uniﬁcador de máxima generalidad (UMG) de (s1 . . . , sn ) y (t1 . . . , tn ) si σ es un uniﬁcador de (s1 . . . , sn ) y (t1 . . . , tn ) más general que cualquier otro. Aplicación de una sustitución a una lista de ecuaciones: (s1 = t1 , . . . , sn = tn )σ = (s1 σ = t1 σ, . . . , sn σ = tn σ). 11 / 31 12.
PD Tema 11: Resolución en lógica de primer orden Uniﬁcación Algoritmo de uniﬁcaciónAlgoritmo de uniﬁcación de listas de términos Entrada: Lista de ecuaciones L = (s1 = t1 , . . . , sn = tn ) y sustitución σ. Salida: Un UMG de las listas (s1 . . . , sn )σ y (t1 . . . , tn )σ, si son uniﬁcables; “No uniﬁcables”, en caso contrario. 12 / 31 13.
PD Tema 11: Resolución en lógica de primer orden Uniﬁcación Algoritmo de uniﬁcaciónAlgoritmo de uniﬁcación de listas de términos Procedimiento unif(L, σ): 1. Si L = (), entonces unif(L, σ) = σ. 2. Si L = (t = t|L ), entonces unif(L, σ) = unif(L , σ). 3. Si L = (f (t1 , . . . , tm ) = f (t1 . . . , tm )|L ), entonces unif(L, σ) = unif((t1 = t1 , . . . , tm = tm |L ), σ). 4. Si L = (x = t|L ) (ó L = (t = x |L )) y x no aparece en t, entonces unif(L, σ) = unif(L [x /t], σ[x /t]). 5. Si L = (x = t|L ) (ó L = (t = x |L )) y x aparece en t, entonces unif(L, σ) = “No uniﬁcables”. 6. Si L = (f (t1 , . . . , tm ) = g(t1 . . . , tm )|L ), entonces unif(L, σ) = “No uniﬁcables”. 7. Si L = (f (t1 , . . . , tm ) = f (t1 . . . , tp )|L ) y m = p, entonces unif(L, σ) = “No uniﬁcables”. 13 / 31 14.
PD Tema 11: Resolución en lógica de primer orden Uniﬁcación Algoritmo de uniﬁcaciónAlgoritmo de uniﬁcación de dos términos Entrada: Dos términos t1 y t2 . Salida: Un UMG de t1 y t2 , si son uniﬁcables; “No uniﬁcables”, en caso contrario. Procedimiento: unif((t1 = t2 ), ). Ejemplo 1: Uniﬁcar f (x , g(z)) y f (g(y ), x ): unif((f (x , g(z)) = f (g(y ), x )), ) = unif((x = g(y ), g(z) = x ), ) por 3 = unif((g(z) = x )[x /g(y )], [x /g(y )]) por 4 = unif((g(z) = g(y )), [x /g(y )]) = unif((z = y ), [x /g(y )]) por 3 = unif((), [x /g(y )][z/y ]) por 4 = unif((), [x /g(y ), z/y ]) = [x /g(y ), z/y ] por 1 14 / 31 15.
PD Tema 11: Resolución en lógica de primer orden Uniﬁcación Algoritmo de uniﬁcaciónEjemplos de uniﬁcación Ejemplo 2: Uniﬁcar f (x , b) y f (a, y ): unif((f (x , b) = f (a, y ), ) = unif((x = a, b = y ), ) por 3 = unif((b = y )[x /a], [x /a]) por 4 = unif((b = y ), [x /a]) = unif((), [x /a][y /b]) por 4 = [x /a, y /b]) por 1 Ejemplo 3: Uniﬁcar f (x , x ) y f (a, b): unif((f (x , x ) = f (a, b)), ) = unif((x = a, x = b), ) por 3 = unif((x = b)[x /a], [x /a]) por 4 = unif((a = b), [x /a]) = “No uniﬁcable” por 6 15 / 31 16.
PD Tema 11: Resolución en lógica de primer orden Uniﬁcación Algoritmo de uniﬁcaciónEjemplos de uniﬁcación Ejemplo 4: Uniﬁcar f (x , g(y )) y f (y , x ): unif((f (x , g(y )) = f (y , x )), ) = unif((x = y , g(y ) = x ), ) por 3 = unif((g(y ) = x )[x /y ], [x /y ]) por 4 = unif((g(y ) = y ), [x /y ]) = “No uniﬁcable” por 5 Ejemplo 5: Uniﬁcar j(w , a, h(w )) y j(f (x , y ), x , z) unif((j(w , a, h(w )) = j(f (x , y ), x , z)) ) = unif((w = f (x , y ), a = x , h(w ) = z), ) por 3 = unif((a = x , h(w ) = z)[w /f (x , y )], [w /f (x , y )]) por 4 = unif((a = x , h(f (x , y )) = z), [w /f (x , y )]) = unif((h(f (x , y )) = z)[x /a], [w /f (x , y )][x /a]) por 4 = unif((h(f (a, y )) = z), [w /f (a, y ), x /a]) = unif((), [w /f (a, y ), x /a][z/h(f (a, y ))]) por 4 = [w /f (a, y ), x /a, z/h(f (a, y ))] por 16 / 31 1 17.
PD Tema 11: Resolución en lógica de primer orden Uniﬁcación Algoritmo de uniﬁcaciónEjemplos de uniﬁcación Ejemplo 6: Uniﬁcar j(w , a, h(w )) y j(f (x , y ), x , y ) unif((j(w , a, h(w )) = j(f (x , y ), x , y )) ) = unif((w = f (x , y ), a = x , h(w ) = y ), ) por 3 = unif((a = x , h(w ) = y )[w /f (x , y )], [w /f (x , y )]) por 4 = unif((a = x , h(f (x , y )) = y ), [w /f (x , y )]) = unif((h(f (x , y )) = y )[x /a], [w /f (x , y )][x /a]) por 4 = unif((h(f (a, y )) = y ), [w /f (a, y ), x /a]) = “No uniﬁcable” por 5 Ejemplo 7: Uniﬁcar f (a, y ) y f (a, b): unif((f (a, y ) = f (a, b), )) = unif((a = a, y = b), ) por 3 = unif((y = b), ) por 2 = unif((), [y /b]) por 4 = [y /b] por 1 17 / 31 18.
PD Tema 11: Resolución en lógica de primer orden Resolución de primer ordenTema 11: Resolución en lógica de primer orden 1. Introducción 2. Uniﬁcación 3. Resolución de primer orden Separación de variables Resolvente binaria Factorización Demostraciones por resolución Adecuación y completitud de la resolución Decisión de no–consecuencia por resolución 18 / 31 19.
PD Tema 11: Resolución en lógica de primer orden Resolución de primer orden Separación de variablesSeparación de variables Def.: La sustitución [x1 /t1 , . . . , xn /tn ] es un renombramiento si todos los ti son variables. Prop.: Si θ es un renombramiento, entonces C ≡ C θ. Def.: Las cláusulas C1 y C2 están separadas si no tienen ninguna variable común. Def.: Una separación de las variables de C1 y C2 es un par de renombramientos (θ1 , θ2 ) tales que C1 θ1 y C2 θ2 están separadas. Ejemplo: Una separación de variables de C1 = {P(x ), Q(x , y )} y C2 = {R(f (x , y ))} es (θ1 = [x /x1 , y /y1 ], θ2 = [x /x2 , y /y2 ]). 19 / 31 20.
PD Tema 11: Resolución en lógica de primer orden Resolución de primer orden Resolvente binariaResolvente binaria Def.: La cláusula C es una resolvente binaria de las cláusulas C1 y C2 si existen una separación de variables (θ1 , θ2 ) de C1 y C2 , un literal L1 ∈ C1 , un literal L2 ∈ C2 y un UMG σ de L1 θ1 y Lc θ2 2 tales que C = (C1 θ1 σ {L1 θ1 σ1 }) ∪ (C2 θ2 σ {L2 θ2 σ}). Ejemplo: Sean C1 = {¬P(x ), Q(f (x ))}, C2 = {¬Q(x ), R(g(x ))}, L1 = Q(f (x )), L2 = ¬Q(x ), θ1 = [x /x1 ], θ2 = [x /x2 ], L1 θ1 = Q(f (x1 )), Lc θ2 = Q(x2 ), 2 σ = [x2 /f (x1 )] Entonces, C = {¬P(x1 ), R(g(f (x1 )))} es una resolvente binaria de C1 y C2 . 20 / 31 21.
PD Tema 11: Resolución en lógica de primer orden Resolución de primer orden FactorizaciónFactorización Def.: La cláusula C es un factor de la cláusula D si existen dos literales L1 y L2 en D que son uniﬁcables y C = Dσ {L2 σ} donde σ es un UMG de L1 y L2 . Ejemplo: Sean D = {P(x , y ), P(y , x ), Q(a)} L1 = P(x , y ) L2 = P(y , x ) σ = [y /x ] Entonces, C = {P(x , x ), Q(a)} es un factor de D. 21 / 31 22.
PD Tema 11: Resolución en lógica de primer orden Resolución de primer orden FactorizaciónEjemplos de refutación por resolución Refutación de S = {{¬P(x , f (x , y ))}, {P(a, z), ¬Q(z, v )}, {Q(u, a)}} 1 {¬P(x , f (x , y ))} Hipótesis 2 {P(a, z), ¬Q(z, v )} Hipótesis 3 {Q(u, a)} Hipótesis 4 {¬Q(f (a, y ), v )} Resolvente de 1 y 2 con σ = [x /a, z/f (a, y )] 5 Resolvente de 3 y 4 con σ = [u/f (a, y ), v /a] Refutación de S = {{P(x )}, {¬P(f (x ))}} 1 {P(x )} Hipótesis 2 {¬P(f (x ))} Hipótesis 3 Resolvente de 1 y 2 con con θ1 = , θ2 = [x /x ], σ = [x /f (x )] 22 / 31 23.
PD Tema 11: Resolución en lógica de primer orden Resolución de primer orden FactorizaciónEjemplos de refutación por resolución Refutación de S = {{P(x , y ), P(y , x )}, {¬P(u, v ), ¬P(v , u)}} 1 {P(x , y ), P(y , x )} Hipótesis 2 {¬P(u, v ), ¬P(v , u)} Hipótesis 3 {P(x , x )} Factor de 1 con [y /x ] 4 {¬P(u, u)} Factor de 2 con [v /u] 5 Resolvente de 3 y 4 con [x /u] 23 / 31 24.
PD Tema 11: Resolución en lógica de primer orden Resolución de primer orden Demostraciones por resoluciónDemostraciones de cláusulas por resolución Sea S un conjunto de cláusulas. La sucesión (C1 , . . . , Cn ) es una demostración por resolución de la cláusula C a partir de S si C = Cn y para todo i ∈ {1, ..., n} se veriﬁca una de las siguientes condiciones: – Ci ∈ S; – existen j, k < i tales que Ci es una resolvente de Cj y Ck – existe j < i tal que Ci es un factor de Cj La cláusula C es demostrable por resolución a partir de S si existe una demostración por resolución de C a partir de S. Una refutación por resolución de S es una demostración por resolución de la cláusula vacía a partir de S. Se dice que S es refutable por resolución si existe una refutación por resolución a partir de S. 24 / 31 25.
PD Tema 11: Resolución en lógica de primer orden Resolución de primer orden Demostraciones por resoluciónDemostraciones de fórmulas por resolución Def.: Sean S1 , . . . , Sn formas clausales de las fórmulas F1 , . . . , Fn y S una forma clausal de ¬F . Una demostración por resolución de F a partir de {F1 , . . . , Fn } es una refutación por resolución de S1 ∪ · · · ∪ Sn ∪ S. Def.: La fórmula F es demostrable por resolución a partir de {F1 , . . . , Fn } si existe una demostración por resolución de F a partir de {F1 , . . . , Fn }. Se representa por {F1 , . . . , Fn } Res F . Ejemplo: (tema 8 p. 21) {∀x [P(x ) → Q(x )], ∃x P(x )} Res ∃x Q(x ) 1 {¬P(x ), Q(x )} Hipótesis 2 {P(a)} Hipótesis 3 {¬Q(z)} Hipótesis 4 {Q(a)} Resolvente de 1 y 2 con [x /a] 5 Resolvente de 3 y 4 con [z/a] 25 / 31 26.
PD Tema 11: Resolución en lógica de primer orden Resolución de primer orden Demostraciones por resoluciónEjemplos de demostraciones por resolución Ejemplo: (tema 8 p. 21) {∀x [P(x ) → Q(x )], ∀x [Q(x ) → R(x )] Res ∀x [P(x ) → R(x )]} 1 {¬P(x ), Q(x )} Hipótesis 2 {¬Q(y ), R(y )} Hipótesis 3 {P(a)} Hipótesis 4 {¬R(a)} Hipótesis 5 {Q(a)} Resolvente de 1 y 3 con [x /a] 6 {R(a)} Resolvente de 5 y 2 con [y /a] 5 Resolvente de 6 y 4 Ejemplo: (tema 6 p. 55) Res ∃x [P(x ) → ∀y P(y )] 1 {P(x )} Hipótesis 2 {¬P(f (x ))} Hipótesis 3 Resolvente de 1 y 2 con θ2 = [x /x ], σ = [x /f (x )] 26 / 31 27.
PD Tema 11: Resolución en lógica de primer orden Resolución de primer orden Demostraciones por resoluciónEjemplos de demostraciones por resolución Ejemplo: Res ∀x ∃y ¬(P(y , x ) ↔ ¬P(y , y )) – Forma clausal: ¬∀x ∃y ¬(P(y , x ) ↔ ¬P(y , y )) ≡ ¬∀x ∃y ¬((P(y , x ) → ¬P(y , y )) ∧ (¬P(y , y ) → P(y , x ))) ≡ ¬∀x ∃y ¬((¬P(y , x ) ∨ ¬P(y , y )) ∧ (¬¬P(y , y ) ∨ P(y , x ))) ≡ ¬∀x ∃y ¬((¬P(y , x ) ∨ ¬P(y , y )) ∧ (P(y , y ) ∨ P(y , x ))) ≡ ∃x ∀y ¬¬((¬P(y , x ) ∨ ¬P(y , y )) ∧ (P(y , y ) ∨ P(y , x ))) ≡ ∃x ∀y ((¬P(y , x ) ∨ ¬P(y , y )) ∧ (P(y , y ) ∨ P(y , x ))) ≡sat ∀y ((¬P(y , a) ∨ ¬P(y , y )) ∧ (P(y , y ) ∨ P(y , a))) ≡ {{¬P(y , a), ¬P(y , y )}, {P(y , y ), P(y , a)}} – Refutación: 1 {¬P(y , a), ¬P(y , y )} Hipótesis 2 {P(y , y ), P(y , a)} Hipótesis 3 {¬P(a, a)} Factor de 1 con [y /a] 4 {P(a, a)} Factor de 2 con [y /a] 27 / 31 28.
PD Tema 11: Resolución en lógica de primer orden Resolución de primer orden Demostraciones por resoluciónParadoja del barbero de Russell En una isla pequeña hay sólo un barbero. El gobernador de la isla ha publicado la siguiente norma: “El barbero afeita a todas las personas que no se afeitan a sí misma y sólo a dichas personas”. Demostrar que la norma es inconsistente. – Representación: ∀x [afeita(b, x ) ↔ ¬afeita(x , x )] – Forma clausal: ∀x [afeita(b, x ) ↔ ¬afeita(x , x )] ≡ ∀x [(afeita(b, x ) → ¬afeita(x , x )) ∧ (¬afeita(x , x ) → afeita(b, x ))] ≡ ∀x [(¬afeita(b, x ) ∨ ¬afeita(x , x )) ∧ (¬¬afeita(x , x ) ∨ afeita(b, x ))] ≡ ∀x [(¬afeita(b, x ) ∨ ¬afeita(x , x )) ∧ (afeita(x , x ) ∨ afeita(b, x ))] ≡ {{¬afeita(b, x ), ¬afeita(x , x )}, {afeita(x , x ), afeita(b, x )}} – Refutación: 1 {¬afeita(b, x ), ¬afeita(x , x )} Hipótesis 2 {afeita(x , x ), afeita(b, x )} Hipótesis 3 {¬afeita(b, b)} Factor de 1 con [x /b] 4 {afeita(b, b)} Factor de 2 con [x /b] 28 / 31 29.
PD Tema 11: Resolución en lógica de primer orden Resolución de primer orden Adecuación y completitud de la resoluciónAdecuación y completitud de la resolución Propiedades: Si C es una resolvente de C1 y C2 , entonces {C1 , C2 } |= C . Si D es un factor de C entonces C |= D. Si ∈ S, entonces S es inconsistente. Si el conjunto de cláusulas S es refutable por resolución, entonces S es inconsistente. Teor.: El cálculo de resolución (para la lógica de primer orden sin igualdad) es adecuado y completo; es decir, Adecuado: S Res F =⇒ S |= F Completo: S |= F =⇒ S Res F 29 / 31 30.
PD Tema 11: Resolución en lógica de primer orden Resolución de primer orden Decisión de no–consecuencia por resoluciónDecisión de no–consecuencia por resolución Enunciado: Comprobar, por resolución, que ∀x [P(x ) ∨ Q(x )] |= ∀x P(x ) ∨ ∀x Q(x ). Reducción 1: Comprobar que es consistente {∀x [P(x ) ∨ Q(x )], ¬(∀x P(x ) ∨ ∀x Q(x ))} Reducción 2: Comprobar que es consistente {{P(x ), Q(x )}, {¬P(a)}, {¬Q(b)}} Resolución: 1 {P(x ), Q(x )} Hipótesis 2 {¬P(a)} Hipótesis 3 {¬Q(b)} Hipótesis 4 {Q(a)} Resolvente de 1 y 2 5 {P(b)} Resolvente de 1 y 3 Modelo: U = {a, b}, I(P) = {b}, I(Q) = {a}. 30 / 31 31.
PD Tema 11: Resolución en lógica de primer orden BibliografíaBibliografía 1. Fitting, M. First-Order Logic and Automated Theorem Proving (2nd ed.) (Springer, 1996) pp. 137–141. 2. M.L. Bonet Apuntes de LPO. (Univ. Politécnica de Cataluña, 2003) pp. 34–40. 3. C.L. Chang y R.C.T. Lee Symbolic logic and mechanical theorem proving (Academic Press, 1973) pp. 70–99. 4. M. Genesereth Computational Logic (Chapter 9: Relational Resolution) (Stanford University, 2003) 5. S. Hölldobler Computational logic. (U. de Dresden, 2004) pp. 71–74. 6. M. Ojeda e I. Pérez Lógica para la computación (Vol. 2: Lógica de Primer Orden) (Ágora, 1997) pp. 138–164. 7. L. Paulson Logic and proof (U. Cambridge, 2002) pp. 50–61. 8. U. Schöning Logic for computer scientists (Birkäuser, 1989) pp. 79–96. 31 / 31 Recommended

References: resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 resolución 
 Resolución 
 Resolución 
 resolución 
 Resolución 
 resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 resolución 
 resolución 
 resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 resolución 
 Resolución 
 Resolución 
 resolución 
 Resolución 
 Resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 Resolución 
 Resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 Resolución 
 Resolución 
 resolución 
 Resolución 
 Resolución 
 resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 resolución 
 resolución 
 Resolución 
 Resolución 
 resolución 
 Resolución