Automatas

Lógica Computacional

José Luis Fernández Vindel Ángeles Manjarrés Riesco Francisco Javier Díez Vegas

Dpto. Inteligencia Artificial

E.T.S.I. Informática UNED 2003

Presentación
Estos apuntes son el embrión de un futuro texto sobre el papel de la lógica en la computación. Han surgido, en principio, como material de estudio de la asignatura Lógica Computacional que los autores impartenen cuarto curso de Ingeniería Informática en la UNED. Quedan aún por desarrollar algunos contenidos. En particular, los que se refieren a la implementación de los sistemas de primer orden, así como un breve recorrido por su uso en computación e inteligencia artificial. El capítulo dedicado a las lógicas modales todavía no hace honor a la enorme explosión teórica y aplicada de este tipo de sistemas enlos últimos años. Por último, obviamente, el capítulo sobre lógica temporal debe ampliarse para recoger, al menos, las lógicas temporales de la computación (tales como CT L∗ y sus subsistemas) y su empleo en la verificación de sistemas reactivos concurrentes. Los capítulos 1-2 y 5-6 están siendo desarrollados por José Luis Fernández Vindel, el capítulo 3 por Ángeles Manjarrés Riesco y el capítulo4 por Francisco Javier Díez Vegas, todos ellos profesores del Departamento de Inteligencia Artificial de la UNED. Agradeceríamos sinceramente cualquier comunicación sobre erratas así como sugerencias sobre los contenidos y su exposición. En particular nos preocupa cómo mantener un tono expositivo amigable sin renunciar al rigor: hasta qué punto facilitar demostraciones formales (y dónde situarlas),cómo reubicar ejemplos y ejercicios para no entorpecer la exposición, etc. La dirección de correo logica4@dia.uned.es está a su disposición para estas comunicaciones, así como la página www.ia.uned.asignaturas/logica4 donde podrá consultar la (inevitable) fe de erratas y el desarrollo de estas notas. Los autores UNED, Madrid, 1 de octubre de 2003

II

Índice general
Introducción Objetivosy contenidos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Motivación para los alumnos de Ingeniería Informática . . . . . . . . . . . . . . . . . . . Bibliografía recomendada . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1 2 3

Parte I. LÓGICA DE PREDICADOS
1 LÓGICA DE PROPOSICIONES Resumen . . . . . . . . . . . . . . . . . . . . . . . . .Objetivos . . . . . . . . . . . . . . . . . . . . . . . . Metodología . . . . . . . . . . . . . . . . . . . . . . . 1.1 Sintaxis . . . . . . . . . . . . . . . . . . . . . . 1.1.1 El lenguaje de la Lógica de Proposiciones 1.1.2 Sobre la estructura inductiva del lenguaje 1.1.3 Derivación de conceptos sintácticos . . . 1.1.4 Eliminación de paréntesis . . . . . . . . 1.2 Semántica . . . . . . . . . . .. . . . . . . . . . 1.2.1 Introducción . . . . . . . . . . . . . . . 1.2.2 Valores de verdad de fórmulas atómicas . 1.2.3 Semántica de las conectivas . . . . . . . 1.2.4 Valores de verdad de fórmulas complejas 1.2.5 Tablas de verdad . . . . . . . . . . . . . 1.2.6 Tautologías y contradicciones . . . . . . 1.3 Conceptos semánticos básicos . . . . . . . . . . 1.3.1 Satisfacibilidad . . . . . . . . .. . . . . 1.3.2 Validez . . . . . . . . . . . . . . . . . . 1.3.3 Consecuencia . . . . . . . . . . . . . . . 1.3.4 Equivalencia . . . . . . . . . . . . . . . 1.4 Sistemas deductivos . . . . . . . . . . . . . . . . 1.4.1 Deducción natural . . . . . . . . . . . . 1.4.2 Resolución . . . . . . . . . . . . . . . . 1.4.3 Tablas semánticas . . . . . . . . . . . . . Bibliografía complementaria . . . . .. . . . . . . . . Actividades y evaluación . . . . . . . . . . . . . . . .

5
7 7 7 8 8 9 12 15 19 20 20 22 22 24 25 26 27 27 29 30 36 42 43 51 57 61 61

. . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . ....