Logica computacional

Lógica Computacional y Demostración Automática
Carlos Areces
areces@loria.fr
http://www.loria.fr/~areces
INRIA Nancy Grand Est, France
Diciembre 2008
El Curso
I En el curso vamos a estudiar varios lenguajes lógicos (lógica
proposicional, lógicas híbridas, lógicas para la descripción,
lógica de predicados) pero desde un punto de vista
computacional.
I Nos interesa en particular estudiardistintos métodos para
determinar cuando una fórmula es satisfacible (i.e., cuando
existe un modelo para una fórmula dada). Aunque también
discutiremos otras tareas de inferencia (e.g., model checking).
I También nos interesa saber cuan complejos son estos
problemas (NP, PSPACE, indecidible).
I Requisitos: Aunque la mayor parte del curso es autocontenida
(i.e., voy a dar todas lasde_niciones necesarias para entender
que estamos haciendo), asumo conocimientos básicos de
lógica, algoritmos y complejidad.
: Lógica Computacional y Demostración Automática INRIA Nancy Grand Est
El Curso
I Miércoles: Lógica Proposicional
+ Método de David-Putnam
+ Métodos Incompletos
+ zcha_ y walksat
I Jueves: Lógicas Híbridas
+ Model Checking
+ mcheck
I Viernes: Lógicas para la Descripción+ Método de Tableaux
+ racer
I Sábado: Lógica de Predicados
+ Método de Resolución
+ spass
: Lógica Computacional y Demostración Automática INRIA Nancy Grand Est
Lo que hacemos hoy
I Consulta Popular: Que saben de lógica?
I Lógica Proposicional
I Una aplicacion simple
I Aplicaciones más interesantes
I Métodos completos
I El método David-Putnam (DP)
I Métodos incompletos
I ElAlgoritmo Greedy
I El Algoritmo GSAT
: Lógica Computacional y Demostración Automática INRIA Nancy Grand Est
Que sabe usted de lógica?
I _, ^,¬,!
I Fórmula Satisfacible, Fórmula Válida (Tautología)
I Tablas de verdad, Método de Tableaux, Método de
Resolución, Método de David-Putnam
I 8x, 9x
I Uni_cación
I 2,3
I @i', #x.'
I 8R.', u, t, v
: Lógica Computacional y Demostración Automática INRIANancy Grand Est
Lógica Computacional = Logica + Computadoras
I La Lógica nació como parte de la _losoía:
I en sus orígenes (allá por la Grecia clásica) la lógica era usada
para modelar el proceso de razonamiento humano
I y para ayudar a derivar inferencias correctas
I Las cosas cambiaron con la llegada de la computadora
I En realidad, la lógica jugó un papel fundamental en el
desarrollo delas computadoras tanto en lo teórico (e.g.,
nociones de computabilidad) como en lo práctico (e.g.,
circuitos lógicos)
I En este curso, vamos a estudiar como la Ciencia de la
Computación contribuye directamente al área de Lógica
: Lógica Computacional y Demostración Automática INRIA Nancy Grand Est
Por que los lógicos necesitamos computadoras?
I Bueno, por empezar, somo humanos y por lotanto vagos. Para
que hacer el trabajo si alguien más puede hacerlo por nosotros?
I Pero aún aquellos raros ejemplares de lógicos energéticos
necesitan ayuda: algunos de los problemas que queremos
resolver son simplemente demasiado complejos para hacer sin
una computadora
I A veces es necesario chequear millones de posibilidades para
veri_car que un sistema satisface una determinada propiedad.I Vamos a ver que, aun usando computadoras, tenemos que
utiliar buenos algoritmos o todo el tiempo del mundo no nos
alcanzaría.
: Lógica Computacional y Demostración Automática INRIA Nancy Grand Est
Lógica Proposicional
I Como todos sabemos la lógica proposicional es fácil:
Algunos simbolos proposicionales: p1, p2, p3, . . .
Dos símbolos lógicos: ¬, _
Dos símbolos sintácticos: (, )
ITambién la semántica es simple:
¬' es verdadera sii ' es falsa
' _ es verdadera sii ' o son verdaderas
I Dada una asignación V de valores de verdad (verdadero o
falso) para todos los símbolos propocisionales podemos
determinar el valor de verdad de de cualquier formula respecto
de V.
: Lógica Computacional y Demostración Automática INRIA Nancy Grand Est
Un problema del corazón
Al...