Universidad de Castilla-La Mancha - Tema 4D - Sistemas...partir de las sentencias atómicas de la...
30
Universidad de Castilla-La Mancha Inteligencia Artificial e Ingeniería del Conocimiento Tema4: Sistemas basados en el conocimiento (Inferencia en Lógica de 1er orden) Profesores: Luis Jiménez Linares. Luis Enrique Sánchez Crespo.
Transcript of Universidad de Castilla-La Mancha - Tema 4D - Sistemas...partir de las sentencias atómicas de la...
Universidad de Castilla-La Mancha Inteligencia Artificial e Ingeniería del Conocimiento
Tema4: Sistemas basados en el
conocimiento (Inferencia en Lógica de 1er orden)
Profesores:
Luis Jiménez Linares.
Luis Enrique Sánchez Crespo.
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
2 de 30
Datos de la Asignatura Temarío
2º Cuatrimestre
Sistemas basados en el conocimiento (Cap. 8-12)
– Mediante lógica de predicados.
– Mediante Sistemas de producción.
Tratamiento de la incertidumbre (Cap. 13-15)
– Redes Bayesianas.
– Razonamiento aproximado (lógica difusa).
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
3 de 30
Inferencia en Lógica 1er Orden
Lógica preposicional vs Lógica de
1er orden
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
4 de 30
Sintaxis y semántica
Reglas de inferencia para cuantificadores:
– Regla de especificación universal: Podemos inferir cualquier sentencia obtenida por sustitución de la variable por un término base (termino sin variables).
– Especificación Existencial: Para cualquier sentencia alfa, variable v, y símbolo de constante k que no aparezca en la base de conocimiento se cumple que
Reducción a la inferencia proposicional: Con las reglas para inferir sentencias no cuantificadas a partir de sentencias cuantificadas, nos es posible reducir la inferencia de primer orden a la inferencia proposicional. La nueva base de conocimiento no es equivalente lógicamente a la antigua, pero se puede demostrar que es equivalente inferencialmente en el sentido que es satisfacible justamente cuando lo es la base de conocimiento original.
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
5 de 30
Inferencia en Lógica 1er Orden
Unificación y Sustitución
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
6 de 30
Unificación y Sustitución
Modus Ponens Generalizado: Se trata de una generalización de las reglas de inferencia aplicando ahora:
– Y-Introducción
– Eliminación Universal
– Modus Ponens
La idea es encontrar la forma de partir de una BC con ciertas oraciones e inferir de allí una nueva oración en un solo paso.
Unificación: Es el proceso que permite a las reglas de inferencia elevadas encontrar las sustituciones que hacen que expresiones lógicas diferentes se hagan idénticas.
Almacenamiento y recuperación:
– Funciones DECIR y PREGUNTAR: utilizadas para informar o interrogar a la base de conocimiento.
– Funcion ALMACENAR(s): guarda una sentencia S en la base de conocimiento.
– Función BUSCAR(q): Devuelve los unificadores que unifican la petición q con alguna sentencia de la base de conocimiento.
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
7 de 30
Unificación y Sustitución Algoritmo de Unificación
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
8 de 30
Unificación y Sustitución
Escanear p y q de izq a der y encontrar el primer término correspondiente s cuando p y q “están en desacuerdo”; cuando p y q no son iguales. Si no hay desacuerdo, retornar theta; buen éxito
Sean, respectivamente, r y s los términos en p y q donde el desacuerdo aparece primero
Si variable ( r ) entonces
theta = union (theta,{r / s})
unificar (sust(theta,p),sust(theta,q),theta)
en el otro caso si variable ( s ) entonces
theta = union (theta,{s / r})
unificar (sust(theta,p),sust(theta,q),theta)
en el otro caso retornar “Falla”
fin
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
9 de 30
Unificación y Sustitución
Es un algoritmo en tiempo lineal que retorna el unificador más general - la lista de sustitución más corta que consigue que haya acuerdo entre dos literales
Aunque en general no hay un único unificador, por lo menos retorna uno que es de longitud mínima
Una variable no puede ser reemplazada por un término que ya contiene dicha variable
– es ilegal x/f(x)
Se debe realizar esa verificación en el seudo-código antes de las llamadas recursivas.
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
10 de 30
Inferencia en Lógica 1er Orden
Algoritmos de Inferencia de
Conocimiento
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
11 de 30
Algoritmos de Inf. Conocimiento
Modus Ponens Generalizado:
– Intentar verificar cada premisa de la implicación
– Unificar cada premisa de la implicación con una oración
atómica existente en la BC, usando solo una sustitución
– ¿Por qué Modus Ponens Generalizado?
• Combina varios pasos en uno
• Usa pasos con garantía de ayudar
• Todas las oraciones están en forma canónica, Forma
Normal de Horn.
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
12 de 30
Algoritmos de Inf. Conocimiento
Encadenamiento hacia delante: Se comienza a partir de las sentencias atómicas de la base de conocimiento, se aplica el Modus Ponens hacia delante, añadiendo las sentencias atómicas nuevas hasta que no se puedan realizar más inferencias. – Añadir una oración p a la BC
– Intentar inferir nuevos hechos usando el Modus Ponens
Generalizado
– Añadir esos nuevos hechos obtenidos con la subrrutina
FORWARD-CHAIN(...)
– Cuando se agotan las informaciones entrantes o las obtenidas por
encadenamiento, el proceso termina hasta tanto ingrese alguna
información nueva.
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
13 de 30
Algoritmos de Inf. Conocimiento
Ejemplo: La ley dice que es un crimen para un americano vender armas a países hostiles. El país de Nono, un enemigo de América, tiene algunos misiles, y todos sus mísiles fueron vendidos por el Coronel West, que es americano.
– << … es un crimen para un americano vender armas a países hostiles>>
Americano(x) Arma(y) Vender(x,y,z) Hostil(z) Criminal(x) (9.3)
– << Nono tiene algunos misiles >>
x Tiene(Nono,x) Misil(x) se convierte en Tiene(Nono,M1) (9.4) y Misil(M1) (9.5)
– << Todos los misiles le (a Nono) fueron vendidos por el coronel West >>
Misil(x) Tiene(Nono,x) Vende(West,x,Nono) (9.6)
Misil(x) Arma(x) (9.7)
Enemigo(x,America) Hostil(x) (9.8)
– << West, que es Americano… >>
Americano(West) (9.9)
– << El país Nono, un enemigo de America… >>
Enemigo(Nono,America) (9.10)
Base de conocimiento Datalog: conjunto de cláusulas de primer orden sin símbolos de función. La ausencia de los símbolos de función hace mucho más fácil la inferencia.
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
14 de 30
Algoritmos de Inf. Conocimiento
Algoritmo sencillo de encadenamiento hacia delante: Comienza con los hechos conocidos, el proceso dispara todas las reglas cuyas premisas se satisfacen, añadiendo sus conclusiones al conjunto de hechos conocidos. El proceso se va repitiendo hasta que la petición es respondida o no se pueden añadir más hechos.
Ejemplo: validar las sentencias de implicación (9.3), (9.6), (9.7) y (9.8)
– Primera iteración:
• La regla (9.3) no tiene satisfechas las premisas.
• La regla (9.6) se satisface con {x/M1}, y se añade Vende(West,M1,Nono)
• La regla (9.7) se satisface con {x/M1}, y se añade Arma(M1)
• La regla (9.8) se satisface con {x/Nono}, y se añade Hostil(Nono).
– Segunda iteración:
• La regla (9.3) se satisface con {x/West, y/M1, z/Nono} y se añade Criminal(West).
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
15 de 30
Algoritmos de Inf. Conocimiento
Árbol de demostración:
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
16 de 30
Algoritmos de Inf. Conocimiento
Encadenamiento hacia delante eficiente: Hay tres fuentes de complejidad posibles:
– Emparejamiento de patrones: El Bucle interno del algoritmo requiere que se encuentren todos los unificadores posibles de manera que la premisa se unifique con un conjunto adecuado de hechos de la base de conocimiento.
– El algoritmo vuelve a comprobar cada regla en cada iteración para ver si sus premisas se satisfacen.
– Podría generar muchos hechos que son irrelevantes para el objetivo.
Hechos irrelevantes: El encadenamiento hacia delante realiza todas las inferencias permitidas basadas en los hechos conocidos, aunque estos sean irrelevantes respecto al objetivo.
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
17 de 30
Algoritmos de Inf. Conocimiento
Algoritmo de Encadenamiento hacia atrás: Estos algoritmos trabajan hacia atrás desde el objetivo, encadenando a través de las reglas hasta encontrar los hechos conocidos que soportan la demostración.
– El algoritmo se invoca con una lista de objetivos que contiene un solo elemento, la petición original, y devuelve el conjunto de todas las sustituciones que satisfacen la petición.
– El algoritmo toma el primero objetivo de la lista y encuentra cada cláusula de la base de conocimiento cuyo literal positivo, o cabeza, se unifica con él.
– Cada una de esta cláusulas crea una nueva llamada recursiva en la que las premisas, o cuerpo, de la cláusulas se añaden a la pila de objetivos.
– Los hechos son cláusulas con cabeza y sin cuerpo.
– Cuando el objetivo se unifica con un hecho conocido, no se añaden más sub-objetivos a la pila, y el objetivo se resuelve.
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
18 de 30
Algoritmos de Inf. Conocimiento
Árbol de demostración:
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
19 de 30
Algoritmos de Inf. Conocimiento
Ejemplo general: “Nintendo dice que es ilegal o criminal para un programador entregar emuladores a la gente. Mis amigos no poseen un Nintendo 64, pero usan soft escrito por RealityMan (un programador) que corre juegos N64 en sus PC.”
– “.. es ilegal para un programador entregar emuladores a la gente..”:
x,y,z Programador(x) Emulador(y) Gente(z) Proveer(x,z,y) Criminal(x) (p1)
– “...Mis amigos usan soft que corre juegos N64…”:
x Usar(MisAmigos, x) Soft(x) Correr(x, JuegosN64) (p2)
– “… soft escrito por RealityMan…”:
x Usar(MisAmigos,x) Soft(x) Correr(x, JuegosN64) Proveer(RealityMan,
MisAmigos, x) (p3)
– Además necesitamos saber que el soft para N64 es un emulador:
x Soft(x) Correr(x, JuegosN64) Emulador(x) (p4)
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
20 de 30
Algoritmos de Inf. Conocimiento
– “...RealityMan (un programador)...”:
Programador(RealityMan) (p5)
– “Mis amigos poseen …”:
Gente(MisAmigos) (p6)
Estos 6 pasos anotados son los estados iniciales de la BC (“axiomas”)
escritos con el idioma de Tarzán (usar, correr)
Demostrar el p2:
– Del paso 3 y de la Eliminación Existencial:
Usar(MisAmigos, UltraHLE) Soft(x) Correr(UltraHLE, JuegoN64) (p7)
– Del paso 7 y de la Y-Eliminación:
Usar(MisAmigos, UltraHLE) (p8)
Soft(UltraHLE) (p9)
Correr(UltraHLE, N64 games) (p10)
x Soft(x) Correr(x, JuegosN64) Emulador(x) (p4)
Soft(UltraHLE) (p9)
Correr(UltraHLE,JuegosN64) (p10)
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
21 de 30
Algoritmos de Inf. Conocimiento
– Del paso 4 y de la Eliminación Universal:
Soft(UltraHLE) Correr(UltraHLE,JuegosN64) Emulador(UltraHLE) (p11)
– De los pasos 9 a 11 y del Modus Ponens: Emulador(UltraHLE) (p12)
x Usar(MisAmigos,x) Soft(x) Correr(x, JuegosN64) Proveer(RealityMan,
MisAmigos, x) (p3)
Usar(MisAmigos, UltraHLE) Soft(x) Runs(UltraHLE, JuegosN64) (p7)
– Del paso 3 y de la Eliminación Universal: Usar(MisAmigos, UltraHLE) Soft(UltraHLE) Correr(UltraHLE, JuegosN64
Proveer(RealityMan, MisAmigos, UltraHLE) (p13)
– De los pasos 7 y 13 y del Modus Ponens: Proveer(RealityMan, MisAmigos, UltraHLE) (p14)
x,y,z Programador(x) Emulador(y) Gente(z) Proveer(x,z,y) Criminal(x) (p1)
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
22 de 30
Algoritmos de Inf. Conocimiento
– Del paso 1 y de la Eliminación Universal: Programador(RealityMan) Emulador(UltraHLE) Gente(MisAmigos)
Proveer(RealityMan, MisAmigos, UltraHLE) Criminal(RealityMan) (p15)
Programador(RealityMan) (p5)
Gente(MisAmigos) (p6)
Emulador(UltraHLE) (p12)
Proveer(RealityMan, MisAmigos, UltraHLE) (p14)
– De pasos 5 a 6 y 12 - y de la Y-Introducción: Programador(RealityMan) Gente(MisAmigos)Emulador(UltraHLE)
Proveer(RealityMan, MisAmigos, UltraHLE) (p16)
Programador(RealityMan) Emulador(UltraHLE) Gente(MisAmigos)
Proveer(RealityMan, MisAmigos, UltraHLE)Criminal(RealityMan) (p15)
– De pasos 15 y 16 y de Modus Ponens: Criminal(RealityMan) (p17)
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
23 de 30
Inferencia en Lógica 1er Orden
Resolución
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
24 de 30
Algoritmos de Inf. Conocimiento
Resolución: La resolución proposicional es un procedimiento de inferencia mediante refutación que es completo para la lógica proposicional.
– La resolución en primer orden requiere que las sentencias estén en la forma normal conjuntiva (FNC – conjunto de cláusulas donde cada cláusula es una disyunción de literales).
– Cada sentencia en lógica de primer orden se puede convertir a una sentencia en FNC que es equivalente inferencialmente.
– Regla de inferencia de resolución: La regla de resolución para la lógica de primer orden es una versión elevada de la regla de resolución proposicional.
– La resolución es un procedimiento de refutación completo, es decir, si un conjunto de sentencias es insatisfacible, entonces la resolución siempre será capaz de derivar una contradicción.
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
25 de 30
Algoritmos de Inf. Conocimiento
Resolución por refutación: – El teorema de refutación permite un método alternativo completo
– Señala dicho Teorema de Refutación:
Si { A } es insatisfactible entonces |= A
– Disponemos de un método mecanizable, correcto y completo: basta
agregar la negación de al fórmula a demostrar y probar la
generación de una cláusula vacía
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
26 de 30
Algoritmos de Inf. Conocimiento
Otras estrategias de resolución: – Resolución unitaria: realiza la resolución sobre cláusulas unitarias.
– Resolución mediante conjunto soporte: Comienza por identificar
un subconjunto de sentencias denominado conjunto soporte. Cada
resolución combina una sentencia del conjunto soporte con otra
sentencia y añade el resolvente al conjunto soporte.
– Resolución lineal: Cada resolución combina una de las sentencias
de entrada con alguna otra sentencia.
– Subsunción: Elimina todas las sentencias que están subsumidas
por una sentencia existente en la BC.
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
27 de 30
Inferencia en Lógica 1er Orden
Resumen
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
28 de 30
Algoritmos de Inf. Conocimiento
Un primer enfoque utiliza reglas de inferencia para instanciar los
cuantificadores y proposicionalizar el problema de inferencia. Por lo
general este enfoque es muy lento.
El uso de la unificación para obtener las sustituciones adecuadas de las
variables elimina el paso de instanciación en las demostraciones de
primer orden, haciendo que el proceso sea mucho más eficiente.
Una versión elevada del Modus Ponens utiliza la unificación para
proporcionar una regla de inferencia natural y potente, el Modus
Ponens Generalizado. Los algoritmos de encadenamiento hacia
delante y de encadenamiento hacia atrás aplican esta regla a
conjuntos de cláusulas positivas.
El Modus Ponens Generalizado es completo para las cláusulas
positivas, aunque el problema de la implicación es semidecidible. Para
los programas Datalog que tiene cláusulas positivas con funciones
libres, la implicación es decidible.
Luis Enrique
Sánchez Crespo
UCLM-ESI Inte
lig
en
cia
Art
ific
ial
e In
gen
ieri
a d
el C
on
ocim
ien
to
29 de 30
Algoritmos de Inf. Conocimiento
El encadenamiento hacia delante se utiliza en las bases de datos deductivas, donde
se pueden combinar con las operaciones de las bases de datos relacionales. También
se utiliza en los sistemas de producción, que pueden hacer actualizaciones
eficientes en conjuntos de reglas muy grandes.
El encadenamiento hacia delante es completo en los programa Datalog y corre en
tiempo polinómico.
El encadenamiento hacia atrás se utiliza en los sistemas de programación lógica
con el Prolog, que emplea una sofisticada tecnología de compilación para
proporcionar una inferencia muy rápida.
El encadenamiento hacia atrás sufre de inferencias redundantes y bucles infinitos;
esto se puede aliviar mediante la memorización.
La regla de inferencia de la resolución generalizada proporciona un sistema de
demostración completo en lógica de primer orden, utilizando bases de conocimiento
en forma normal conjuntiva.
Existen diversas estrategias para reducir el espacio de búsqueda de un sistema de
resolución sin comprometer la completitud. Los demostradores de teoremas
eficientes, basados en la resolución, se han utilizado para proporcionar teoremas
matemáticos de interés y para verificar y diseñar hardware y software.
Universidad de Castilla-La Mancha
Luis Jiménez Linares
Luis Enrique Sánchez Crespo
