Tenemos la base. Hagamos visible el motor.
01Hacia adelante: partir de hechos y obtener consecuencias.
02Hacia atrás: partir de una meta y buscar una prueba.
03Después: reconocer unificación y resolución.
Modus ponens, una vez más.
01Tenemos α → β y también α.
02Podemos derivar β.
03Con varias premisas, necesitamos que todas se cumplan.
α → β, α ⊢ β
No inventar conclusiones.
01Todo lo derivado debe seguirse lógicamente de la base.
02Si las premisas son verdaderas, una inferencia correcta preserva verdad.
03La corrección del motor no garantiza que las observaciones estén bien cargadas.
No perder conclusiones que sí se siguen.
01Un motor completo puede obtener todas las consecuencias del lenguaje y fragmento considerados.
02Correcto pero incompleto: lo que obtiene está justificado, aunque puede omitir resultados.
03Hay que declarar sobre qué fragmento y procedimiento se da la garantía.
¿Qué falla si falta una conclusión?
Las reglas no están escritas como instrucciones del programa.
01Cada regla tiene id, lista de premisas y conclusión.
02Los hechos se representan con un conjunto.
03El mismo motor puede trabajar con otra base del mismo formato.
{"id": "R2",
"si": ["problema_alimentacion", "cable_ok"],
"entonces": "fuente_danada"}Derivar hasta que nada nuevo se habilite.
01Comenzar con los hechos conocidos.
02Revisar reglas y agregar conclusiones cuando todas sus premisas estén presentes.
03Repetir hasta completar el recorrido sin nuevos disparos.
De los hechos al cierre.
Hechos disponibles en este paso
no_enciendesin_luz_fuentecable_ok
Meta: reemplazar_fuente
Ver reglas en su orden
- R1
no_enciende ∧ sin_luz_fuente → problema_alimentacion - R2
problema_alimentacion ∧ cable_ok → fuente_danada - R3
no_enciende ∧ hay_luz_fuente → problema_placa - R4
fuente_danada → reemplazar_fuente - R5
problema_placa ∧ pitidos → revisar_memoria
Partimos de los hechos
Observaciones iniciales: no_enciende, sin_luz_fuente, cable_ok. Todavía no aplicamos reglas.
- Partimos de los hechos
La condición de disparo está en all().
01Todas las premisas deben pertenecer a hechos.
02usadas evita disparar indefinidamente la misma regla.
03traza conserva la justificación de cada disparo.
if all(p in hechos for p in r["si"]):
hechos.add(r["entonces"])
usadas.add(r["id"])
traza.append((r["id"], r["si"], r["entonces"]))
cambio = TrueMismo cierre, distinto recorrido.
01Una conclusión nueva puede habilitar reglas que ya pasamos de largo.
02El bucle externo vuelve a revisarlas.
03La base es finita y cada regla se dispara como máximo una vez en este programa.
Una conclusión necesita una procedencia.
01R1: observaciones → problema_alimentacion.
02R2: problema_alimentacion + cable_ok → fuente_danada.
03R4: fuente_danada → reemplazar_fuente.
R1 → R2 → R4
Empezar por lo que queremos demostrar.
01Si la meta ya es un hecho, está probada.
02Si no, buscar reglas que la concluyan.
03Demostrar sus premisas como subobjetivos, y reconstruir la respuesta.
Una pregunta se convierte en subpreguntas.
Hechos iniciales
no_enciendesin_luz_fuentecable_ok
Meta: reemplazar_fuente
Ver reglas en su orden
- R1
no_enciende ∧ sin_luz_fuente → problema_alimentacion - R2
problema_alimentacion ∧ cable_ok → fuente_danada - R3
no_enciende ∧ hay_luz_fuente → problema_placa - R4
fuente_danada → reemplazar_fuente - R5
problema_placa ∧ pitidos → revisar_memoria
Elegimos una meta
Buscamos demostrar reemplazar_fuente; no la agregamos como hecho.
- Elegimos una metaNivel 0
Antes de bajar otra vez, comprobar y cortar.
01Objetivo en hechos: devolver True.
02Objetivo ya en esta rama: cortar el ciclo.
03En otro caso, buscar una regla y probar todas sus premisas.
if objetivo in hechos:
return True
if objetivo in visitados:
return False
visitados = visitados | {objetivo}No consultado no significa falso.
01all() con un generador se detiene en el primer False.
02Para revisar_memoria se intenta problema_placa antes que pitidos.
03Si falla problema_placa, esta rama no llega a consultar pitidos.
all(probar(p, reglas, hechos, nivel + 2, visitados)
for p in r["si"])A necesita B. B necesita A.
01Una dependencia circular no aporta una prueba por sí sola.
02Se corta la rama que repite una meta en curso.
03Después pueden intentarse otras reglas que concluyan la misma meta.
b → a · a → b · ¿hay un apoyo externo?
¿Qué comprobó realmente la búsqueda?
La pregunta de trabajo cambia el recorrido.
01Adelante: hechos → consecuencias; útil cuando llegan datos y queremos sus efectos.
02Atrás: meta → subobjetivos; útil ante una consulta concreta.
03Ambos pueden gastar trabajo en reglas o ramas que no resultan útiles.
Leer una regla no es intentar demostrarla.
01El Python hacia atrás recorre la lista para buscar conclusiones coincidentes.
02Para revisar_memoria intenta R5 y R3, pero también inspecciona otras entradas.
03Los contadores distinguen inspecciones de lista y comprobaciones o intentos.
Llegan lecturas y necesitamos reaccionar.
Buscar una sustitución consistente.
01Unificar significa volver idénticas dos expresiones mediante sustituciones.
02Cada aparición de una misma variable debe recibir un valor compatible.
03Los dos motores anteriores trabajan con átomos concretos, sin este mecanismo.
Padre(x, maría) · Padre(juan, y)
Una variable, el mismo reemplazo.
Expresiones a comparar
Padre(x, maría)Padre(juan, y)Comparar expresiones
Buscamos una única sustitución consistente en todas las posiciones.
- Comparar expresiones
La regla general llega al caso.
01Regla: Hombre(x) → Mortal(x), con x universal.
02Hecho: Hombre(sócrates).
03Sustitución: x = sócrates, también en el consecuente.
Mortal(sócrates)
Suponer la negación de la meta y buscar contradicción.
01Queremos probar que β se sigue de la base.
02Agregamos ¬β y trabajamos con cláusulas.
03Si derivamos la cláusula vacía □, la refutación está completa.
De P → Q y P, demostrar Q.
Cláusulas y premisas disponibles
P → QP
Meta: Q
Base y objetivo
Base: P → Q y P. Objetivo: demostrar Q.
- Base y objetivo
Completa para refutar no significa que siempre termine.
01La resolución ofrece completitud por refutación con la preparación y estrategia adecuadas.
02En primer orden no hay garantía general de terminación cuando la meta no se sigue.
03La igualdad requiere tratamiento adicional; nuestro ejemplo es proposicional.