Inferencias de lógica preposicional

Prerrequisito: Mundo Wumpus en Inteligencia Artificial

El agente utiliza la inferencia lógica para identificar qué casillas son seguras, pero hace planes a través de una búsqueda A ^* . En esta parte, le mostraremos cómo construir planes utilizando la inferencia lógica. El concepto básico es sencillo:

1. Escribe una frase que comprenda
   • , un conjunto de afirmaciones sobre el estado inicial;
   • , los axiomas del estado sucesor para todas las acciones concebibles en cada momento hasta un tiempo máximo  ; y
   • la afirmación de que el objetivo se alcanza en el momento  : 
2. A un solucionador de SAT, presente la declaración completa. El objetivo se logra si la solución desarrolla un modelo adecuado; si la frase es insatisfactoria, el problema de planificación es imposible.
3. Suponiendo que haya encontrado un modelo, extraiga las variables que indican acciones y configúrelas como verdaderas. Forman una estrategia para alcanzar los objetivos.

 Inferencias de lógica preposicional

SATP _LAN es una técnica de planificación proposicional. Promulga el concepto general mencionado anteriormente, pero con un giro. El algoritmo prueba cada número potencial de pasos t, hasta una longitud máxima probable del plan Tmax, porque el agente no sabe cuántos pasos tomará para alcanzar la meta. Se garantiza encontrar el plan más corto si existe uno de esta manera. Esta estrategia no puede ser empleada en un ambiente parcialmente observable por la forma en que SATP _LAN busca una solución; SATP _LAN simplemente establecería las variables no observables en los valores necesarios para construir una solución.

La creación de la base de conocimiento es un paso crucial en el uso de SATP _LAN . Superficialmente, los axiomas del mundo wumpus parecen ser suficientes para los pasos 1(a) y 1(b) anteriores. Los requisitos de vinculación (según la evaluación de  ) y los de satisfacibilidad, por otro lado, son muy diferentes. Considere la ubicación inicial del agente de  , y diga que el objetivo modesto del agente es estar en   el momento 1.   está en la base de conocimiento inicial y   es el objetivo. Podemos establecer   usando   si se afirma Forward ⁰ , pero no podemos probar L12,1 si, por ejemplo, se afirma Shoot0 en su lugar. SATPLAN ahora está buscando el plan [Forward0]; Hasta ahora, todo bien. Sin embargo, SATP _{LAN también detecta el plan [Shoot}⁰ ]. ¿Como es posible? Para averiguarlo, examinamos el modelo de SATPLAN, que incluye la asignación  , que establece que el agente puede estar en [2,1] en el momento 1 estando allí en el momento 0 y disparando. «¿No mencionamos que el agente está en   el momento 0?» uno podría preguntarse. ¡Sí, pero no le informamos al agente que no podía estar en dos lugares al mismo tiempo!  es desconocido para la implicación y, por lo tanto, no puede usarse en una prueba; por otra parte,  es desconocido para la satisfacibilidad y, por lo tanto, se puede establecer en cualquier valor que ayude a hacer realidad el objetivo. Como resultado, SATPLAN es una herramienta de depuración útil para bases de conocimiento porque identifica brechas de conocimiento. Podemos arreglar la base de conocimiento en este escenario afirmando que el agente está exactamente en una ubicación en cada paso de tiempo, utilizando un conjunto de frases similares a las que se utilizan para indicar la existencia de un wumpus preciso. Para todas las ubicaciones que no sean  , podemos reclamar  ; el axioma del estado sucesor para la ubicación se encarga de pasos de tiempo adicionales. Se pueden usar los mismos ajustes para garantizar que el agente solo tenga una orientación.

SATP _LAN , por otro lado, tiene algunas sorpresas más guardadas. La primera es que busca modelos que realicen actividades imposibles, como disparar una flecha sin ella. Para entender por qué necesitamos echar un vistazo más de cerca a lo que implican los axiomas del estado sucesor sobre acciones con condiciones previas no satisfechas. Los axiomas son verdaderos al predecir que nada sucederá si se lleva a cabo tal acción, ¡pero no son correctos al afirmar que la acción no puede llevarse a cabo! Para evitar producir planes que contengan acciones ilegales, debemos incluir axiomas de condiciones previas que establezcan que para que ocurra una acción, se deben cumplir las condiciones previas. Por ejemplo, necesitamos decir eso   para cada vez  .

Esto asegura que si un plan elige la acción Disparar en cualquier momento, el agente debe tener una flecha en la pantalla en ese momento. La formulación de planes con varias acciones simultáneas es la segunda sorpresa de SATP _{LAN .} Puede, por ejemplo, generar un modelo en el que tanto Forward0 como Shoot0 sean verdaderos, lo cual no está permitido. Introducimos axiomas de exclusión de acciones para resolver este problema: para cada par de acciones   y  , agregamos el axioma  .

Cabe señalar que dar un paso adelante y disparar al mismo tiempo no es difícil, sin embargo, disparar y agarrar al mismo tiempo, por ejemplo, es bastante poco práctico. Podemos permitir planes con muchas acciones simultáneas al imponer axiomas de exclusión de acciones solo en pares de actividades que realmente interfieren entre sí, y debido a que SATP _LAN determina el plan legal más corto, podemos estar seguros de que hará uso de esta capacidad.

Para resumir, SATP _LAN busca modelos en una oración que contiene los axiomas de estado inicial, objetivo, estado sucesor, axiomas de condición previa y axiomas de exclusión de acción. Puede demostrarse que este conjunto de axiomas es suficiente, en el sentido de que no existen más “soluciones” falsas. Cualquier modelo que cumpla con el enunciado proposicional es una solución viable al problema en cuestión. La estrategia es bastante realista gracias a las modernas tecnologías de resolución de SAT. Un solucionador de estilo DPLL, por ejemplo, no tiene problemas para proporcionar la solución de 11 pasos para la instancia del mundo wumpus.

El enfoque declarativo de la construcción de agentes discutido en esta sección es que el agente funciona afirmando declaraciones en la base de conocimiento y haciendo inferencias lógicas. Algunas fallas en este enfoque están disfrazadas en términos como «para cada tiempo t» y «para cada cuadrado [x, y]». cualquier agente práctico. Podríamos necesitar un   tablero y 1000 pasos de tiempo para un mundo wumpus de tamaño razonable, similar a un pequeño juego de computadora, que resulte en bases de conocimiento con decenas o cientos de millones de frases. Esto no solo es poco práctico, sino que también resalta un problema mayor: sabemos algo sobre el mundo wumpus, a saber, que elLa «física» funciona de la misma manera en todos los cuadrados y pasos de tiempo, algo que no podemos describir explícitamente en la lógica proposicional. Necesitamos un lenguaje más expresivo para manejar este desafío, uno que permita que palabras como “para cada vez t” y “para cada cuadrado [x,y]” se escriban de forma natural. Un mundo wumpus de cualquier tamaño y duración se puede describir en alrededor de 10 oraciones en lugar de diez millones o diez billones en lógica de primer orden.