El algoritmo DPLL en Coq

El algoritmo DPLL en Coq Fernando Abigail Galicia Mendoza Forma normal conjuntiva FNC conjuntista Satisfacibilidad El algoritmo Davis-PutnamLogemannLoveland Una ejecuci´ on

El algoritmo DPLL en Coq Fernando Abigail Galicia Mendoza

¿Porqu´ e usar Coq?

Facultad de ciencias, UNAM Cuarta escuela de l´ ogica y conjuntos

7 de diciembre de 2015

El algoritmo DPLL en Coq

Forma normal conjuntiva

Fernando Abigail Galicia Mendoza Forma normal conjuntiva FNC conjuntista Satisfacibilidad El algoritmo Davis-PutnamLogemannLoveland Una ejecuci´ on ¿Porqu´ e usar Coq?

Definici´ on (Forma normal conjuntiva) Una f´ ormula de la l´ ogica proposicional est´ a en forma normal conjuntiva (FNC), si es generada por la siguiente gr´ amatica: At´ omicas a ::= > | ⊥ | p con con p una variable proposicional Literales ` ::= a | ¬a Cla´ usulas C ::= ` | ` ∨ C Formas normales conjuntivas C ::= C | C ∧ C

Proposici´ on Cualquier f´ ormula proposicional ϕ puede transformarse algor´ıtmicamente en una f´ ormula ψ tal que ϕ ≡ ψ y ψ est´ a en FNC, donde ϕ ≡ ψ denota que ϕ y ψ son f´ ormulas l´ ogicamente equivalentes.

El algoritmo DPLL en Coq

Forma normal conjuntiva (Parte 2)

Fernando Abigail Galicia Mendoza Forma normal conjuntiva FNC conjuntista Satisfacibilidad El algoritmo Davis-PutnamLogemannLoveland Una ejecuci´ on ¿Porqu´ e usar Coq?

Ejemplo • La forma normal conjuntiva de p ↔ q es (¬p ∨ q) ∧ (¬q ∨ p). • La forma normal conjuntiva de p → ((q → r ) → ¬s) es

(¬p ∨ q ∨ ¬s) ∧ (¬p ∨ ¬r ∨ ¬s). • La forma normal conjuntiva de p ↔ (q → r ) es

(¬p ∨ ¬q ∨ r ) ∧ (p ∨ q) ∧ (p ∨ ¬r ). Observemos que esta representaci´ on de la forma normal conjuntiva es ineficiente para m´etodos de resoluci´ on sint´ acticos.

El algoritmo DPLL en Coq Fernando Abigail Galicia Mendoza Forma normal conjuntiva FNC conjuntista Satisfacibilidad El algoritmo Davis-PutnamLogemannLoveland

FNC conjuntista De ahora en adelante asumiremos que dada una f´ ormula en FNC ϕ esta no tenga cla´ usulas repetidas, ni literales at´ omicas (>,⊥).

Definici´ on Sea C una una cl´ ausula en FNC, definimos la FNC conjuntista (FNCC) de C como el conjunto de todas sus literales, es decir, si C = `1 ∨ · · · ∨ `n su FNCC es {`1 , . . . , `n }.

Una ejecuci´ on ¿Porqu´ e usar Coq?

Definici´ on Dada ϕ una f´ ormula en FNC, definimos la FNCC de ϕ como el conjunto de todas sus cl´ ausulas en FNCC, es decir, si ϕ = C1 ∧ · · · ∧ Cn su FNCC es {C1 , . . . , Cn }.

Ejemplo • La FNCC de (¬p ∨ q) ∧ (¬q ∨ p) es {{¬p, q}, {¬q, p}}. • La FNCC de (¬p ∨ ¬q ∨ r ) ∧ (p ∨ q) ∧ (p ∨ ¬r ) es

{{¬p, ¬q, r }, {p, q}, {p, ¬r }}.

El algoritmo DPLL en Coq

Satisfacibilidad

Fernando Abigail Galicia Mendoza Forma normal conjuntiva FNC conjuntista Satisfacibilidad El algoritmo Davis-PutnamLogemannLoveland Una ejecuci´ on ¿Porqu´ e usar Coq?

Definici´ on (El problema de satisfacibilidad) Dada una f´ ormula de la l´ ogica proposicional saber si existe una asignaci´ on de valores para sus variables tales que hagan la f´ ormula satisfacible.

Definici´ on Sea M un conjunto de literales, ϕ una f´ ormula de la l´ ogica proposicional y IM : PROP → {0, 1} una funci´ on de interpretaci´ on, se dice que M es modelo de ϕ si IM (ϕ) = 1.

Ejemplo Veamos que p ↔ (q → r ) es satisfacible. Sea M = {p, ¬q}, por demostrar que IM (p ↔ (q → r )) = 1. Por definici´ on tenemos que, IM (p ↔ (q → r )) = 1 si y solo si IM (p) = IM (q → r ). Observamos que IM (q) = 0, entonces IM (q → r ) = 1. Y se tiene que IM (p) = 1. Por lo que p ↔ (q → r )) es satisfacible.

El algoritmo DPLL en Coq

El algoritmo Davis-Putnam-Logemann-Loveland

Fernando Abigail Galicia Mendoza Forma normal conjuntiva FNC conjuntista Satisfacibilidad El algoritmo Davis-PutnamLogemannLoveland Una ejecuci´ on ¿Porqu´ e usar Coq?

El algoritmo Davis-Putnam-Logemann-Loveland (DPLL) es un procedimiento que recibe una f´ ormula FNC conjuntista y devuelve un modelo.

Definici´ on Sean ` una literal, ` la literal contraria de `, C una cla´ usula conjuntista, C una f´ ormula en FNCC y M un modelo. Denotemos a M es modelo de C como M ` C. El procedimiento del algoritmo DPLL est´ a dado por las siguientes reglas de inferencia:

El algoritmo DPLL en Coq

El algoritmo Davis-Putnam-Logemann-Loveland (Parte 2)

Fernando Abigail Galicia Mendoza Forma normal conjuntiva

Definici´ on (Parte 2)

FNC conjuntista Satisfacibilidad El algoritmo Davis-PutnamLogemannLoveland Una ejecuci´ on ¿Porqu´ e usar Coq?

M`∅

M ∪ {`} ` C Unit M ` C ∪ {{`}}

Satis

M ∪ {`} ` C ∪ C M ∪ {`} ` C ∪ {{`} ∪ C }

Red

M ∪ {`} ` C Elim M ∪ {`} ` C ∪ {{`}} ∪ C }

M ∪ {`} ` C M ∪ {`} ` C Split M`C

Teorema (Correctud de algoritmo DPLL) Para toda C una f´ ormula en FNCC, existe un modelo M devuelto por el algoritmo DPLL con entrada C tal que M ` C.

El algoritmo DPLL en Coq

Una ejecuci´on

Fernando Abigail Galicia Mendoza Forma normal conjuntiva FNC conjuntista Satisfacibilidad El algoritmo Davis-PutnamLogemannLoveland Una ejecuci´ on ¿Porqu´ e usar Coq?

Ejemplo Hagamos la ejecuci´ on del algoritmo para la f´ ormula p ↔ q, como se mencion´ o su FNCC es [[¬p, q] , [¬q, p]]. X C [p, q] ` ∅ [¬p, q] ` [[]] X [p, q] ` [[p]] [¬p, ¬q] ` ∅ [¬p, q] ` [[p]] [p, q] ` [[¬q, p]] [¬p, ¬q] ` [[¬q, p]] [¬p, q] ` [[¬q, p]] [p] ` [[q] , [¬q, p]] [¬p] ` [[¬q, p]] [p] ` [[¬p, q] , [¬q, p]] [¬p] ` [[¬p, q] , [¬q, p]] ∅ ` [[¬p, q] , [¬q, p]] Observemos que el algoritmo devolvi´ o tres conjuntos de variables proposicionales, donde [¬p, q] no satisface a la f´ ormula, ya que es propenso a causar inconsistencia, es decir, tener a p y ¬p.

El algoritmo DPLL en Coq

¿Porqu´e usar Coq?

Fernando Abigail Galicia Mendoza Forma normal conjuntiva FNC conjuntista Satisfacibilidad El algoritmo Davis-PutnamLogemannLoveland Una ejecuci´ on ¿Porqu´ e usar Coq?

• Por la misma definici´ on que brindan sus autores, Coq es un asistente

para generar demostraciones por computadora evitando errores humanos, con esto tenemos una prueba certificada del algoritmo DPLL. • Hay que observar que el paso de demostraciones hechas en papel a

Coq es un paso interesante, ya que en papel se asumen ciertas cosas que en Coq debemos demostrarlas o darlas como axiomas. • Se opt´ o por utilizar listas en lugar de conjuntos debido a que las listas

son un tipo primitivo en los lenguajes de programaci´ on.

El algoritmo DPLL en Coq

Referencias

Fernando Abigail Galicia Mendoza Forma normal conjuntiva FNC conjuntista Satisfacibilidad El algoritmo Davis-PutnamLogemannLoveland Una ejecuci´ on ¿Porqu´ e usar Coq?

St´ephane Lescuyer, Sylvain Conchon. (-). Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme. Noviembre de 2015, de Laboratoire de Recherche En Informatique Sitio web: https:// www.lri.fr/~conchon/publis/lescuyer-conchon-frocos09.pdf Varios. (-). What is Coq?. Noviembre de 2015, de The Coq proof assistant Sitio web: https://coq.inria.fr/