Download teorema lógica -principios -representación

Document related concepts
no text concepts found
Transcript
Agentes Lógicos
Capítulo 7
Agentes lógicos
•
•
•
•
•
•
Agentes de conocimiento básico
Mundo de Wumpus
Lógica en general – modelos y sus vínculos
Proposición de lógica (Booleana)
Equivalencia, validez
Reglas de inferencia y demostración del
teorema
– encadenamiento hacia delante
– encadenmiento hacia atrás
– resolución
Conocimientos básicos
• Knowledge base = conjunto de sentencias en lenguaje formal
•
• Declaración apropiada para construir un agente (u otro sistema):
– Decir lo que necesita saber
• Entonces puede preguntarse qué hacer – las respuestas provienen
de la KB
• Los agentes pueden verse en el nivel de conocimiento
Es decir lo que ellos saben, sin tener en cuenta como lo implementaron
• O al nivel de implementación
– Es decir, los datos de la estructura en la KB pueden ser manipulados
por ellos
–
Un simple agente basado en
conocimiento
• El agente pude ser capaz de:
•
– Representar estados, acciones, etc.
–
– Incorporar nuevos preceptos
–
– Actualizar representaciones internas del mundo
–
Descripcion del espacio
Wumpus PEAS
• Evaluación del desempeño
– oro +1000, muerte -1000
– -1 por paso, -10 por usar la flecha
• Ambiente
•
–
–
–
–
–
–
–
Cuadros adyacentes a wumpus apestan (s)
Cuadros adyacentes a un pozo tiene brisa (b)
El cuadro donde está el oro brilla (g)
Si disparas en la dirección de Wumpus, lo matas
Al disparar usas la única flecha
La acción agarrar, toma el oro si está en el mismo lugar
La acción soltar, deja el oro en el mismo lugar
• Sensores: Stench, Breeze, Glitter, Bump, Scream
•
• Actuadores: Left turn, Right turn, Forward, Grab, Release, Shoot
Caracteristicas del espacio
Wumpus
• Se Observa todo No – solo tenemos perepción
local
• Determinístico Si –Los resultados son exactos y
específicos
• Episódico No – secuencial en el nivel de
acciones
• Estático Si – Wumpus y Pits no se mueven
•
• Discreto Si
• Agente-único Si
Explorando el espacio wumpus
Explorando un espacio wumpus
Explorando un espacio wumpus
Explorando un espacio wumpus
Explorando un espacio wumpus
Explorando un espacio wumpus
Explorando un espacio wumpus
Explorando un espacio wumpus
Lógica en general
• La lógica es el lenguaje formal para representar la
información de modo que se puedan obtener
conclusiones
• Syntaxis define las sentencias en el lenguaje
• Semanticas define el “significado" de las sentencias;
– i.e., define truth of a sentence in a world
• v.g., el lenguaje de aritmética
–
–
–
–
x+2 ≥ y es correcto; x2+y > {} no es correcto
x+2 ≥ y es verdadero ssi x+2 no es menor que y
x+2 ≥ y es verdadero en un mundo donde x = 7, y = 1
x+2 ≥ y es falso en un mundo donde x = 0, y = 6
Consecuencias lógicas
• Entailment (consecuencia lógica) medios que vinculan
una cosa con otra:
•
KB ╞ α
• Una sentencia α es consecuencia lógica de la base de
conocimiento KB si y soloy si α es verdadera en todos
los espacios donde KB es verdadera
– Por ejemplo el KB que contiene “los Giants ganaron” y “los Reds
ganaron” relaciona “los Giants ganaron o los Reds ganaron”
– Por ejemplo, x+y = 4 relaciona 4 = x+y
–
– Entailment es una relación entre las frases (es decir, sintaxis)
eso es basado en la semántica
Modelos
• Típicamente, un logista piensa en términos de modelos, con
estructuras formales de espacio con respecto a la verdad con la que
son evaluadas
•
• Nosotros decimos que una sentencia m es un modelo de α si α es
verdadera en m
• M(α) es el conjunto de todos
los modelos de α
• Entonces KB ╞ α si M(KB)  M(α)
Por ejemplo KB = Giants y Reds ganaron
α = Giants ganaron
Razonando en el mundo de wumpus
Situación después de no
descubrir nada en [1,1],
moviendo a la [2,1]
Considere posibles modelos
para KB asumiendo solo
hoyos
3 opciones boleanas
 8 posibles modelos
Modelos Wumpus
Modelos Wumpus
• KB = wumpus-espacio dominio + observaciones
Modelos Wumpus
• KB = wumpus-espacio dominio + observaciones
• α1 = "[1,2] es seguro, KB ╞ α1, probado por verificación de
modelo
Modelos Wumpus
• KB = wumpus-espacio dominio + observaciones
Modelos Wumpus
• KB = wumpus-epacio dominio + observaciones
• α2 = [2,2] es seguro, KB ╞ α2
•
Inferencia
• KB ├i α = sentencia α puede ser derivada de KB por
procedimiento i
•
• Seguridad: i es seguro siempre que cuando KB ├i α,sea
también verdad que KB╞ α
•
• Completitud: i es completo siempre que cuando KB╞ α,
sea también verdad que KB ├i α
•
• Se definirá una lógica (lógica de primer orden) con poder
expresivo para decir casi cualquier cosa interesante
• Esto es, el procedimiento contestará cualquier pregunta
cuya respuesta sea una consecuencia lógica de KB.
Lógica Proposicional: Syntaxis
• La lógica proposicional es una lógica muy
• Los símbolos de proposición P1, P2, etc. son sentencias
–
–
–
–
–
–
–
–
–
–
Si S es una fórmula, S también lo es (negación)
Si S1 y S2 son fórmulas, S1  S2 también lo es (conjunción)
Si S1 y S2 son fórmulas, S1  S2 también lo es (disyunción)
Si S1 y S2 son fórmulas, S1  S2 también lo es (implicación)
Si S1 y S2 son fórmulas, S1  S2 también lo es (bicondicional)
Lógica Proposicional: Semántica
Cada modelo especifica true/false para símbolo proposicional
v.g.
P1,2
false
P2,2
true
P3,1
false
Con estos símbolos, 8 pocibles modelos, pueden enumerarse automáticamente.
Regla para evaluación respecto al modelo m:
S
es verdadero ssi S is false
S1  S2 es verdadero ssi S1 es verdadero and S2 es verdadero
S1  S2 es verdadero ssi S1 es verdadero or S2 es verdadero
S1  S2 es verdadero ssi S1 es falso or S2 es verdadero
i.e., es verdadero ssi S1 es verdadero and S2 es falso
S1  S2 es verdadero ssi S1S2 is true andS2S1 is true
Un simple proceso recursivo para evaluar una sentencia arbitraria,
v.g., P1,2  (P2,2  P3,1) = true  (true  false) = true  true = true
Tablas de verdad para
conectividades
Sentencias del espacio Wumpus
Let Pi,j be true if there is a pit in [i, j].
Let Bi,j be true if there is a breeze in [i, j].
 P1,1
B1,1
B2,1
• “Los hoyos causan brisa en cuadros
adyacentes"
B1,1 
B2,1 
(P1,2  P2,1)
(P1,1  P2,2  P3,1)
Tablas de verdad para inferencia
Inferencia por enumeración
• Enumeración por profundidad de todos los modelos es segura y
completa
• Para n símbolos, complejidad en tiempo O(2n), complejidad en
espacio es O(n)
•
Equivalencia lógica
• Dos expresiones son lógicamente equivalentes si son
verdad en el mismo modelo: α ≡ ß iff α╞ β and β╞ α
Validez y Satisfacibilidad
Un expresion es válida si es verdadera en todos los modelos,
v.g., True,
A A, A  A, (A  (A  B))  B
La validez está relacionada con la inferencia vía el Theorema de
Deducción:
KB ╞ α ssi (KB  α) es válida
Una expresión es satisfacible si es verdadera en algún modelo
v.g., A B,
C
Una expresión es inválida si no es verdadera en ningún modelo
v.g., AA
La satisfacibilidad está relacionada con la inferencia via:
KB ╞ α Si y solo si (KB α) is insatisfacible
Métodos de Prueba
• Los métodos de prueba se dividen en dos tipos
– Applicación de la regla de inferencia
• Generación Legítima (segura) de nuevas expresiones a partir de las
viejas
• Prueba = Secuencia de reglas de inferencia en aplicaciones
Puede usarse la regla de inferencia como operador en una
búsqueda estandar
• Típicamente requiere la transformación de la expresión de
sentencias en una forma normal
– Chequeo de Modelo
• Para enumerar la tabla (siempre es exponencial en n)
• Backtracking, v.g., Davis--Putnam-Logemann-Loveland (DPLL)
• La búsqueda en el espacio de modelos (segura, incompleta)
v.g., min-conflicts-like hill-climbing algorithms
Resolución
Forma Normal Conjuntiva (CNF)
conjunción de disyunciones de las literales
v.g., (A  B)  (B  C  D)
• Resolución regla de interferencia (for CNF):
li …  lk,
m1  …  mn
li  …  li-1  li+1  …  lk  m1  …  mj-1  mj+1 ...  mn
Donde li y mj son literales complementarias.
v.g., P1,3  P2,2,
P2,2
P1,3
• La resolución es legítima y completa para
la lógica proposicional
Resolución
Regla de resolución:
(li  …  li-1  li+1  …  lk)  li
mj  (m1  …  mj-1  mj+1 ...  mn)
(li  …  li-1  li+1  …  lk)  (m1  …  mj-1  mj+1 ...  mn)
Conversión a CNF
B1,1  (P1,2  P2,1)β
1. Eliminar , reemplazar α  β con (α  β)(β  α).
(B1,1  (P1,2  P2,1))  ((P1,2  P2,1)  B1,1)
2. Eliminar , reemplazar α  β con α β.
(B1,1  P1,2  P2,1)  ((P1,2  P2,1)  B1,1)
3. Mover  introduciendo la regla de D´Morgan y la doble
negación:
(B1,1  P1,2  P2,1)  ((P1,2  P2,1)  B1,1)
4. Aplicar distributividad ( encima ) y reorganizar:
(B1,1  P1,2  P2,1)  (P1,2  B1,1)  (P2,1  B1,1)
Algoritmo de Resolución
• Prueba por contradicción. v.g. demostrar KBα es
inválida
Ejemplo
• KB = (B1,1  (P1,2 P2,1))  B1,1 α = P1,2
•
Forward and backward chaining
•
Horn Clauses (restringido)
KB = conjunción de cláusulas de Horn
– Clausula de Horn
• Símbolo de proposición; o
• (símbolo de conjunción)  símbolo
– v.g. C  (B  A)  (C  D  B)
• Modus Ponens (para cláusulas de Horn)
α1, … ,αn,
α 1  …  αn  β
β
• Puede usarse con encadenamiento hacia adelante o hacia atrás
• El algoritmo es muy natural y corre en tiemo real
Forward chaining
• La Idea: utilizar cualquier regla cuyas premisas son
satisfechas en la KB,
• Crear una conclusión para la KB, hasta que la búsqueda
tenga éxito
Agoritmo de Forward chaining
• El encadenamiento hacia adelante es válido y
completo para KBs de Horn
Ejemplo de Forward chaining
Ejemplo de Forward chaining
Ejemplo de Forward chaining
Ejemplo de Forward chaining
Ejemplo de Forward chaining
Ejemplo de Forward chaining
Ejemplo de Forward chaining
Ejemplo de Forward chaining
Prueba de Completitud
•
FC deriva cada sentencia atómica que es
consecuencia lógica de la KB
1. FC alcanza un punto donde no hay nuevas
expresiones que derivar
2. Considerar el estado final como un modelo m,
asignando true/false a símbolos
3. Cada cláusula en la KB original es verdadera en m
a1  …  ak  b
4. Por consiguiente m es un modelo de KB
5. si KB╞ q, q es verdadera en todo modelo de KB,
incluyendo m
Backward Chaining
Idea: trabajar hacia atrás partiendo del query q
Para demostrar q por BC,
Observar si q es ya conocida, o
Demostrar mediante BC que se cumplen todas las premisas de
alguna regla que concluye q
Evite las vueltas: observe si la nueva submeta ya está en
el stack
Evite trabajar de más: observe si la nueva submeta
1. Ya se ha demostrado verdadera, or
2. Ya se ha demostrado falsa
Ejemplo de Backward Chaining
Ejemplo de Backward Chaining
Ejemplo de Backward Chaining
Ejemplo de Backward Chaining
Ejemplo de Backward Chaining
Ejemplo de Backward Chaining
Ejemplo de Backward Chaining
Ejemplo de Backward Chaining
Ejemplo de Backward Chaining
Ejemplo de Backward Chaining
Forward Chaining
vs. Backward Chaining
• FC es un proceso dirigido por los datos, automático,
inconsciente
– v.g. reconocimiento de objetos, elecciones de rutina
• Puede hacer muchos trabajo irrelevante a la meta
• BC es un proceso dirigido por la meta, apropiado para la
solución de problemas,
– v.g. ¿Donde están mis llaves? ¿Cómo entro al programa PhD?
• La complejidad de BC puede ser mucho menor que
linear en el tamaño de KB
Inferencia Proposicional Eficiente
Dos familias de algoritmos eficientes para inferencia
proposicional:
Algoritmos de búsqueda con backtracking completo
• Algoritmos DPLL (Davis, Putnam, Logemann, Loveland)
• Algoritmos de búsqueda locales incompletos
– WalkSAT
El algoritmo DPLL
Determinar si una entrada lógica proporcional (en CNF) es satisfacible
Mejoras a la tabla de verdad:
1. Terminación temprana
Una cláusula es verdadera si cualquier literal es verdadera.
Una expresión es falsa si cualquier cláusula es falsa.
2. Heurística Simbólica Pura
Símbolo puro:siempre aparece con el misma signo en todas las cláusulas.
v.g. en (A  B), (B  C), (C  A), A y B son puras, C es impura.
Hacer verdadero a un símbolo puro
3. Heurística de cláusula unitaria
Cláusula Unitaria: solo una literal en la cláusula
La única literal en la cláusula debe ser verdad
El algoritmo DPLL
El algoritmo WalkSAT
• Algoritmo Incompleto de búsqueda local
• Función de Evaluació: La heurística de mínimo conflicto
de minimizar el número de cláusulas insatisfechas
• Equilibrio entre voracidad y aletoreidad
El algoritmo WalkSAT
Problemas de satisfacibilidad
difíciles
• Considere sentencias 3-CNF aleatorias
(D  B  C)  (B  A  C)  (C 
B  E)  (E  D  B)  (B  E  C)
m = número de cláusulas
n = número de símbolos
– Los problemas difíciles parecen aglutinarse
cerca de m/n = 4.3 (punto crítico)
Problemas de satisfacibilidad
difíciles
Problemas de satisfacibilidad
difíciles
• Mediana tiemo de corrida para 100 satisfactible
al azar 3-CNF sentencias, n = 50
•
Agentes basados en Inferencia
para el mundo de wumpus
Un agente en el mundo de wumpus usando lógica
proposicional:
P1,1
W1,1
Bx,y  (Px,y+1  Px,y-1  Px+1,y  Px-1,y)
Sx,y  (Wx,y+1  Wx,y-1  Wx+1,y  Wx-1,y)
W1,1  W1,2  …  W4,4
W1,1  W1,2
W1,1  W1,3
…
 64 símbolos proposicionales distintos, 155 sentencias
Límites de expresividad de la
lógica proposicional
• KB contienesentencias “físicas” para cada cuadro
t
• t Para cada tiempo t y cada posición
[x,y],
Lx,y  FacingRightt  Forwardt  Lx+1,y
• Rápida proliferación de cláusulas
Summary
• Los agentes lógicos aplican inferencia a una base de conocimiento
para derivar nueva información y tomar desiciones
• Conceptos básicos de logica:
–
–
–
–
–
–
sintaxis: estructura formal de sentencias
semántica: veracidad de sentencias con respecto a modelos
consecuencia: la verdad necesaria de una sentencia dada otra
inferencia: derivar sentencias de otras sentencias
seguridad: sólo produce consecuencias lógicas
completitud: las derivaciones pueden producir todas las consecuencias
lógicas
• El espacio Wumpus requiere de abilidad para representar
información parcial y negada, razonamiento por casos, etc.
• Resolución es completa para la lógica proposicional
Forward y Backward Chaining son completos y lineales para
cláusulas de Horn
• La lógica proposicional carece de poder expresivo