Ver el código de «Formal Correctness Proof for DPLL Procedure»

Pilip Marić y Predrag Janicić (2009)
[http://argo.matf.bg.ac.rs/publications/2009/DPLL_correctness_proof.pdf Formal Correctness Proof for DPLL Procedure]. Aceptado en ''Informatica''. Pendiente de publicación.
----
En este trabajo se presenta la formalización en Isabelle/Isar de una demostración de la corrección del procedimiento DPLL (Davis-Putnam-Logemann-Loveland). La formalización se encuentra [http://argo.matf.bg.ac.rs/downloads/formalizations/ClassicDPLL.zip classic DPLL procedure]. Aunque afirma que es la primera formalización de DPLL, en el artículo [http://www.cs.us.es/~jalonso/publicaciones/2004-JAR.pdf Formal Verification of a Generic Framework to Synthesize SAT-Provers] (Journal of Automated Reasoning. Vol. 32. Núm. 4. 2004. Pag. 287-313) se presenta una formalización del procedimiento DPLL en ACL2 con la demostración en ACL2 de su corrección.

La estructura del trabajo es la siguiente
# '''Introducción''' en la que se presenta el problema SAT, el procedimiento DPLL, sus mejoras, su papel en los modernos SAT y sus aplicaciones. Me ha parecido interesante las razones que justifican la formalización (1) algunos SMT de los que han participado en las competiciones no son adecuados y (2) el trabajo incrementa el conocimiento matemático formalizado. 
# '''Antecedentes''' donde comenta el procedimiento DPLL  junto con comentarios sobre Isabelle, Isar y la verificación de programas.
# '''Notaciones y definiciones''' donde presenta las notaciones, definiciones (de variable, literal, cláusula, fórmula e interpretación, variable de un literal, literal complementario, ocurrencia de un literal en una fórmula, conjuntos de variables de una cláusula (de una fórmula y de una interpretación), cuando un literal (cláusula o fórmula) es verdadero (o falso) en una interpretación, interpretaciones consistentes, modelo de una fórmula),  y las proposiciones básicas de la formalización en Isabelle. 
# '''Formalización del procedimiento DPLL''' 
## '''Sustituciones''' en donde define la sustitución de un literal de una fórmula por un booleano, enuncia las propiedades básicas de la sustitución y demuestra el lema de bifurcación.
## '''Cláusulas unitarias''' en donde define las cláusulas unitarias y demuestra el lema de las cláusulas unitarias.
## '''Literales puros''' en donde define los literales puros y el lema de los literales puros.
## ''' Definición del procedimiento DPLL''' en donde define el procedimiento DPLL en donde los procedimientos auxiliares sólo son especificados. Una definición de los procedimientos auxiliares se da en el apéndice.
## '''Terminación y corrección del procedimiento DPLL''' en donde demuestra la terminación del procedimiento a partir de la dismininución del número de literales y la corrección por inducción
# '''Formalización en Isabelle/Isar''' en donde presenta la definición en Isabelle/Isar del procedimiento DPLL y la demostración de su corrección.
# '''Trabajos relacionados''' donde comenta algunas formalizaciones en Isabelle y las descripciones abstractas de DPLL.
# '''Conclusiones y trabajos futuros''' donde vuelve a repetir que es la primera formalización de DPLL (aunque anteriormente comentamos la realizada en ACL2) y propone continuar la tarea formalizando la corrección de buscadores SAT y SMT correspondientes a las actuales implementaciones.

[[User:Jalonso|José A. Alonso]] 20:34, 10 April 2009 (CEST)
[[Category:Lecturas]]