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 S1S2 is true andS2S1 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., AA 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