Laboratorio: Espacio de Modelos, Vinculación y Satisfacibilidad

Explora cómo una Base de Conocimiento ($KB$) restringe mundos posibles, cómo se evalúa $KB \models f$ y cómo se reducen las operaciones Ask y Tell a pruebas SAT.

Configuración de la Base de Conocimiento (KB) M(KB) = ⋂ M(f)
Cada fórmula añadida a la KB actúa como un filtro: descarta mundos imposibles. Inicialmente hay $2^3 = 8$ modelos. A medida que aprendes hechos, el conjunto $M(KB)$ se reduce y el conocimiento del agente es más preciso.
Espacio de Mundos Posibles (Modelos w) Modelos válidos: 8/8
Modelo compatible con KB
Modelo descartado
Consulta al Sistema Lógico Ask[f] / Tell[f]
Selecciona una consulta para evaluar la relación semántica con la KB actual.
Relaciones fundamentales:
  • Vinculación ($KB \models f$): $M(KB) \subseteq M(f)$. En todo mundo compatible con KB, $f$ es verdadera.
  • Contradicción ($KB \models \neg f$): $M(KB) \cap M(f) = \emptyset$. Imposible que ocurran juntos.
  • Contingencia: $f$ es verdadera en algunos modelos de KB y falsa en otros. Ni $f$ ni $\neg f$ se pueden asegurar.
Visualización de Inclusión de Modelos M(KB) vs M(f)
M(KB)
M(f)
Intersección M(KB) ∩ M(f)
Árbol de Decisión: Reducción de Inferencia a Satisfactibilidad (Diapositiva 22) ¿Es KB ∪ {¬f} satisfactible?

En lugar de generar todas las combinaciones de la tabla de verdad, podemos delegar cualquier pregunta lógica Ask[f] o Tell[f] a un solucionador de satisfactibilidad (SAT solver).

Haz clic en "Evaluar en árbol" o cambia la consulta en la pestaña anterior para ver la ruta tomada.
Formulación de Lógica Proposicional como CSP (Diapositiva 23) Variables booleanas + Restricciones de arcos

Ejemplo de la diapositiva 23: $KB = \{A \vee B, B \leftrightarrow \neg C\}$. Cada símbolo proposicional es una variable CSP con dominio $\{0, 1\}$. Las fórmulas lógicas se convierten en restricciones binarias entre nodos.

Restricciones de arco:
  • Arco (A, B): $A \vee B \equiv \text{No }(A=0 \wedge B=0)$. Pares válidos: $(0,1), (1,0), (1,1)$.
  • Arco (B, C): $B \leftrightarrow \neg C \equiv B \neq C$. Pares válidos: $(0,1), (1,0)$.
Soluciones del CSP (Modelos de KB):
Calculando...