Hispanopedia Wiki
Articulo de referencia

Compresión de prueba

En la teoría de la demostración , un área de la lógica matemática , la compresión de demostraciones es el problema de comprimir algorítmicamente las demostraciones formales . Lo...

Hispanopedia WikiContenido en espanolLectura gratuita

En la teoría de la demostración , un área de la lógica matemática , la compresión de demostraciones es el problema de comprimir algorítmicamente las demostraciones formales . Los algoritmos desarrollados pueden utilizarse para mejorar las demostraciones generadas por herramientas automatizadas de demostración de teoremas , como los solucionadores SAT , los solucionadores SMT , los demostradores de teoremas de primer orden y los asistentes de demostración .

Representación del problema

En lógica proposicional, una prueba de resolución de una cláusulaκ{\displaystyle \kappa }A partir de un conjunto de cláusulas C, se obtiene un grafo acíclico dirigido (DAG): los nodos de entrada son inferencias axiomáticas (sin premisas) cuyas conclusiones son elementos de C , los nodos resolventes son inferencias de resolución y la prueba tiene un nodo con conclusión.κ{\displaystyle \kappa }. [ 1 ]

El DAG contiene una arista desde un nodo.η1{\displaystyle \eta _{1}}a un nodoη2{\displaystyle \eta _{2}}si y solo si una premisa deη1{\displaystyle \eta _{1}}es la conclusión deη2{\displaystyle \eta _{2}}. En este caso,η1{\displaystyle \eta _{1}}es hijo deη2{\displaystyle \eta _{2}}, yη2{\displaystyle \eta _{2}}es padre deη1{\displaystyle \eta _{1}}Un nodo sin hijos es una raíz.

Un algoritmo de compresión de pruebas intentará crear un nuevo DAG con menos nodos que represente una prueba válida deκ{\displaystyle \kappa }o, en algunos casos, una prueba válida de un subconjunto deκ{\displaystyle \kappa }.

Un ejemplo sencillo

Tomemos una prueba de resolución para la cláusula{a,b,do}{\displaystyle \left\{a,b,c\right\}}del conjunto de cláusulas

{η1:{a,b,pag},η2:{do,¬pag}}η1:a,b,pagη2:do,¬pagη3:a,b,dopag{\displaystyle \left\{\eta _{1}:\left\{a,b,p\right\},\eta _{2}:\left\{c,\neg p\right\}\right\}\quad {\frac {\eta _{1}:a,b,p\quad \quad \eta _{2}:c,\neg p}{\eta _{3}:a,b,c}}p}

Aquí podemos ver:

  • η1{\displaystyle \eta _{1}}yη2{\displaystyle \eta _{2}}son nodos de entrada.
  • El nodoη3{\displaystyle \eta _{3}}tiene un pivotepag{\displaystyle p},
    • izquierda resuelta literalpag{\displaystyle p}
    • correcto resuelto literal¬pag{\displaystyle \neg p}
  • η3{\displaystyle \eta _{3}}conclusión es la cláusula{a,b,do}{\displaystyle \left\{a,b,c\right\}}
  • η3{\displaystyle \eta _{3}}Las premisas son la conclusión de los nodos.η1{\displaystyle \eta _{1}}yη2{\displaystyle \eta _{2}}(sus padres)
  • El DAG sería
η1η2↖ ↗η3{\displaystyle {\begin{array}{ccc}\eta _ {1}&&\eta _ {2}\\&\nwarrow \nearrow \\&\eta _ {3}\end{array}}}
  • η1{\displaystyle \eta _{1}}yη2{\displaystyle \eta _{2}}son padres deη3{\displaystyle \eta _{3}}
  • η3{\displaystyle \eta _{3}}es hijo deη1{\displaystyle \eta _{1}}yη2{\displaystyle \eta _{2}}
  • η3{\displaystyle \eta _{3}}es una raíz de la prueba

Una refutación (de resolución) de C es una prueba de resolución de⊥{\displaystyle \bot }de C. Es común dar un nodoη{\displaystyle \eta }, para referirse a la cláusulaη{\displaystyle \eta }oη{\displaystyle \eta }cláusula de 's que significa la cláusula de conclusión deη{\displaystyle \eta }y (sub)pruebaη{\displaystyle \eta }lo que significa que la (sub)prueba tieneη{\displaystyle \eta }como su única raíz.

En algunos trabajos se puede encontrar una representación algebraica de inferencias de resolución . La resolvente deκ1{\displaystyle \kappa _{1}}yκ2{\displaystyle \kappa _{2}}con pivotepag{\displaystyle p}puede denotarse comoκ1⊙pagκ2{\displaystyle \kappa _{1}\odot _{p}\kappa _{2}}Cuando el pivote está definido de forma única o es irrelevante, lo omitimos y escribimos simplementeκ1⊙κ2{\displaystyle \kappa _{1}\odot \kappa _{2}}De esta forma, el conjunto de cláusulas puede verse como un álgebra con un operador conmutativo; y los términos en el álgebra de términos correspondiente denotan pruebas de resolución en un estilo de notación más compacto y más conveniente para describir pruebas de resolución que la notación gráfica habitual.

En nuestro último ejemplo, la notación del DAG sería{a,b,pag}⊙pag{do,¬pag}{\displaystyle \left\{a,b,p\right\}\odot _{p}\left\{c,\neg p\right\}}o simplemente{a,b,pag}⊙{do,¬pag}.{\displaystyle \left\{a,b,p\right\}\odot \left\{c,\neg p\right\}.}

Podemos identificar{a,b,pag}⏞η1⊙{do,¬pag}⏞η2⏟η3{\displaystyle \underbrace {\overbrace {\left\{a,b,p\right\}} ^{\eta _{1}}\odot \overbrace {\left\{c,\neg p\right\}} ^{\eta _{2}}} _{\eta _{3}}}.

algoritmos de compresión

Los algoritmos para la compresión de demostraciones de cálculo secuencial incluyen la introducción de cortes y la eliminación de cortes .

Los algoritmos para la compresión de pruebas de resolución proposicional incluyen RecycleUnits , [ 2 ] RecyclePivots , [ 2 ] RecyclePivotsWithIntersection , [ 1 ] LowerUnits , [ 1 ] LowerUnivalents , [ 3 ] Split , [ 4 ] Reduce&Reconstruct , [ 5 ] y Subsumption .

Notas

  1. 1 2 3 Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno. Compresión de pruebas de resolución proposicional mediante regularización parcial . 23.ª Conferencia sobre Deducción Automatizada , 2011.
  2. 1 2 Bar-Ilan, O.; Fuhrmann, O.; Hoory, S.; Shacham, O.; Strichman, O. Reducciones en tiempo lineal de pruebas de resolución . Hardware y software: verificación y pruebas, págs. 114-128, Springer, 2011.
  3. ↑ "Skeptik/Doc/Papers/LUniv en develop · Paradoxika/Skeptik · GitHub" . GitHub .{{cite web}}: CS1 maint: servicio de archivado obsoleto ( enlace )
  4. ↑ Cotton, Scott. " Dos técnicas para minimizar las pruebas de resolución ". XIII Conferencia Internacional sobre Teoría y Aplicaciones de las Pruebas de Satisfacibilidad, 2010.
  5. ↑ Simone, SF; Brutomesso, R.; Sharygina, N. " Un enfoque eficiente y flexible para la reducción de pruebas de resolución ". 6.ª Conferencia de Verificación de Haifa, 2010.