El mecanismo de identificar, aislar o generar lemas intermedios o candidatos a lemas a partir de pruebas, trazas de búsqueda u heurísticas para acelerar, estructurar o habilitar la reutilización en pasos de razonamiento posteriores.

Principio

Capturar hechos intermedios recurrentes o útiles que compriman la estructura de la prueba y reduzcan la redundancia; los lemas de alta calidad son lo bastante generales para reutilizarse entre subobjetivos pero lo bastante específicos para podar eficazmente búsquedas futuras.

Demostración

Un probador automático registra cláusulas de conflicto de una búsqueda SAT como lemas para evitar revisitar la misma asignación conflictiva; un asistente de pruebas extrae patrones de prueba usados con frecuencia en lemas nombrados para acortar pruebas interactivas futuras; heurísticas inductivas proponen lemas que generalizan un patrón hallado en un intento de prueba fallido.

Aplicación incorrecta

Extraer lemas demasiado específicos que solo encajan en una traza de prueba (conduciendo a fragmentación y sobrecarga de almacenamiento), o extraer lemas incorrectos debido a instrumentación defectuosa que luego corrompe el razonamiento y produce resultados no válidos.

Consecuencia

La extracción eficaz de lemas mejora la modularidad de las pruebas, reduce la búsqueda redundante, permite bibliotecas y caché de lemas, y puede convertir búsquedas exponenciales en tratables; sin embargo, malas elecciones de lemas pueden aumentar la sobrecarga y desviar la búsqueda.

Inversión

Búsqueda de prueba monolítica que nunca registra ni reutiliza lemas intermedios: cada subobjetivo se redescubre repetidamente, a menudo con gran coste; por el contrario, lemas sobregeneralizados pueden borrar la estructura y hacer que las pruebas sean frágiles.

Límite

La calidad de los lemas extraídos depende de la heurística de extracción, la estructura del dominio y la verificación de la corrección de los lemas; la extracción no es una panacea: algunos dominios generan pocos lemas reutilizables y algunos esquemas de extracción son costosos de calcular.

Tensión semántica

Entre la generalidad y la utilidad del lema: los lemas generales maximizan la reutilización pero corren el riesgo de ser demasiado débiles para podar la búsqueda; los lemas muy específicos podan bien a nivel local pero rara vez se transfieren entre problemas.

Síntesis

La extracción de lemas identifica y registra proposiciones intermedias que destilan patrones de razonamiento recurrentes; una extracción y validación juiciosas crean bloques reutilizables que comprimen pruebas, aceleran la búsqueda y apoyan el razonamiento modular, reconociendo a la vez los compromisos en generalidad, corrección y costes de almacenamiento.