Formal Correctness Proof for DPLL Procedure
Revisión del 16:15 10 abr 2009 de Jalonso (discusión | contribuciones) (New page: 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''. Pe...)
Pilip Marić y Predrag Janicić (2009) 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 classic DPLL procedure.
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. Aunque afirma que es la primera formalización de DPLL, nosotros ya hemos pubicado una formalización en
