Libro.logicaComputacional

Lógica Computacional

Lic. Wilber Ramos Lovón

7 de noviembre de 2010

Índice general

I Introducción 80.1. Etapa matemática . . . . . . . . . . . . . . . . . . . . . . . . . . 130.2. Etapa computacional . . . . . . . . . . . . . . . . . . . . . . . . . 19

II Los Fundamentos 24

1. Una Panorámica de la Programación Declarativa 251.1. Computadores y Lenguajes de Programación . . . . . . . 251.2. Programación Declarativa . . . . . . . . . . . . . . . . . . . 271.3. Programación Lógica - Programación Funcional . . . . 281.4. Comparación con los Lenguajes Imperativos y Áreas de

Aplicación . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 311.4.1. Diseño del Lenguaje y Escritura de Programas 321.4.2. Mantenimiento . . . . . . . . . . . . . . . . . . . . . . . 351.4.3. Coste y Eficiencia . . . . . . . . . . . . . . . . . . . . 35

1.5. Lista de Ejercicios . . . . . . . . . . . . . . . . . . . . . . . . . . 37

2. Sistemas Formales y Lógica de Proposiciones 392.1. Sistemas Formales . . . . . . . . . . . . . . . . . . . . . . . . 39

2.1.1. Observación: . . . . . . . . . . . . . . . . . . . . . . . . 392.2. Lógica de Proposiciones: Sintaxis . . . . . . . . . . . . . . . 40

2.2.1. Definición: (Sistema Formal) . . . . . . . . . . . . . 402.2.2. Operadores Booleanos . . . . . . . . . . . . . . . . . . . . 412.2.3. Definición: . . . . . . . . . . . . . . . . . . . . . . . . . . 432.2.4. Ejemplo: . . . . . . . . . . . . . . . . . . . . . . . . . . . 432.2.5. Teorema: . . . . . . . . . . . . . . . . . . . . . . . . . . . 452.2.6. Definición: . . . . . . . . . . . . . . . . . . . . . . . . . . 452.2.7. Teorema: (Inducción Estructural) . . . . . . . . . . . . . 46

2.3. Lógica de Proposiciones: Semántica . . . . . . . . . . . . . 462.3.1. Definición: . . . . . . . . . . . . . . . . . . . . . . . . . . . 462.3.2. Ejemplo: . . . . . . . . . . . . . . . . . . . . . . . . . . . 462.3.3. Teorema: . . . . . . . . . . . . . . . . . . . . . . . . . . . 472.3.4. Teorema: . . . . . . . . . . . . . . . . . . . . . . . . . . . 472.3.5. Definición: . . . . . . . . . . . . . . . . . . . . . . . . . . . 47

1

ÍNDICE GENERAL 2

2.3.6. Ejemplo: . . . . . . . . . . . . . . . . . . . . . . . . . . . . 472.3.7. Definición: . . . . . . . . . . . . . . . . . . . . . . . . . . . 472.3.8. Ejemplo: . . . . . . . . . . . . . . . . . . . . . . . . . . . . 482.3.9. Teorema: . . . . . . . . . . . . . . . . . . . . . . . . . . . 482.3.10. Observación: . . . . . . . . . . . . . . . . . . . . . . . . . 482.3.11. Teorema: . . . . . . . . . . . . . . . . . . . . . . . . . . . 482.3.12. Definición: . . . . . . . . . . . . . . . . . . . . . . . . . . . 492.3.13. Ejemplo: . . . . . . . . . . . . . . . . . . . . . . . . . . . . 492.3.14. Definición: . . . . . . . . . . . . . . . . . . . . . . . . . . . 492.3.15. Ejemplo: . . . . . . . . . . . . . . . . . . . . . . . . . . . . 492.3.16. Teorema: . . . . . . . . . . . . . . . . . . . . . . . . . . . 492.3.17. Fórmulas Lógicamente Equivalentes . . . . . . . . . . . . 492.3.18. Observaciones: . . . . . . . . . . . . . . . . . . . . . . . . 512.3.19. Definición: . . . . . . . . . . . . . . . . . . . . . . . . . . . 512.3.20. Ejemplo: . . . . . . . . . . . . . . . . . . . . . . . . . . . . 512.3.21. Teorema: . . . . . . . . . . . . . . . . . . . . . . . . . . . 51

2.4. Satisfacibilidad , Validez y Consecuencia . . . . . . . . . 522.4.1. Definición: . . . . . . . . . . . . . . . . . . . . . . . . . . 522.4.2. Teorema: . . . . . . . . . . . . . . . . . . . . . . . . . . . 522.4.3. Definición: . . . . . . . . . . . . . . . . . . . . . . . . . . . 522.4.4. Observación: . . . . . . . . . . . . . . . . . . . . . . . . . 522.4.5. Ejemplo: . . . . . . . . . . . . . . . . . . . . . . . . . . . . 532.4.6. Ejemplo: . . . . . . . . . . . . . . . . . . . . . . . . . . . . 532.4.7. Ejemplo: . . . . . . . . . . . . . . . . . . . . . . . . . . . . 532.4.8. Definición: . . . . . . . . . . . . . . . . . . . . . . . . . . . 532.4.9. Ejemplo: . . . . . . . . . . . . . . . . . . . . . . . . . . . . 532.4.10. Teorema: . . . . . . . . . . . . . . . . . . . . . . . . . . . 542.4.11. Teorema: . . . . . . . . . . . . . . . . . . . . . . . . . . . 542.4.12. Definición: . . . . . . . . . . . . . . . . . . . . . . . . . . . 542.4.13. Ejemplo: . . . . . . . . . . . . . . . . . . . . . . . . . . . . 542.4.14. Teorema: . . . . . . . . . . . . . . . . . . . . . . . . . . . 542.4.15. Teorema: . . . . . . . . . . . . . . . . . . . . . . . . . . . 542.4.16. Observación: . . . . . . . . . . . . . . . . . . . . . . . . . 54

2.5. Tableau Semántico . . . . . . . . . . . . . . . . . . . . . . . . 552.5.1. Definición: . . . . . . . . . . . . . . . . . . . . . . . . . . 552.5.2. Ejemplo: . . . . . . . . . . . . . . . . . . . . . . . . . . . . 552.5.3. Ejemplo: . . . . . . . . . . . . . . . . . . . . . . . . . . . . 562.5.4. Definición: . . . . . . . . . . . . . . . . . . . . . . . . . . 572.5.5. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . 582.5.6. Observación : . . . . . . . . . . . . . . . . . . . . . . . . 582.5.7. Ejemplo . . . . . . . . . . . . . . . . . . . . . . . . . . . . 582.5.8. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . 582.5.9. Corolario: . . . . . . . . . . . . . . . . . . . . . . . . . . 582.5.10. Corolario : . . . . . . . . . . . . . . . . . . . . . . . . . . 582.5.11. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 58

2.6. Lógica Proposicional : Sistemas Deductivos . . . . . . . . 59

ÍNDICE GENERAL 3

2.6.1. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 592.6.2. Observación : . . . . . . . . . . . . . . . . . . . . . . . . 592.6.3. El Sistema de Gentzen G . . . . . . . . . . . . . . . . . . 60

2.6.3.1. Definición : . . . . . . . . . . . . . . . . . . . . 602.6.4. Observacion : . . . . . . . . . . . . . . . . . . . . . . . . . 612.6.5. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 612.6.6. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 622.6.7. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 622.6.8. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . . 632.6.9. Corolario : . . . . . . . . . . . . . . . . . . . . . . . . . . 632.6.10. Teorema : ( Solidez y Compleción de G ) . . . . . . . . . 63

2.7. El Sistema de Hilbert H . . . . . . . . . . . . . . . . . . . . 632.7.1. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 632.7.2. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . 642.7.3. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 642.7.4. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 652.7.5. Regla de la Deducción : . . . . . . . . . . . . . . . . . . . 652.7.6. Teorema de la deducción : . . . . . . . . . . . . . . . . . . 652.7.7. Observación: . . . . . . . . . . . . . . . . . . . . . . . . . 652.7.8. Regla Contrapositiva : . . . . . . . . . . . . . . . . . . . . 652.7.9. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . . 652.7.10. Regla de la Transitividad : . . . . . . . . . . . . . . . . . 662.7.11. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . 662.7.12. Regla de Intercambio de Antecedentes : . . . . . . . . . . 662.7.13. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . . 662.7.14. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . . 672.7.15. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . . 672.7.16. Regla de la Doble Negación : . . . . . . . . . . . . . . . . 672.7.17. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . . 682.7.18. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . . 682.7.19. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . . 692.7.20. Regla de la Deducción al Absurdo : . . . . . . . . . . . . . 692.7.21. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . . 692.7.22. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . . 69

2.8. Teoremas de otros operadores . . . . . . . . . . . . . . . . . . . . 702.8.1. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . . 702.8.2. Teorema : ( debilitamiento ) . . . . . . . . . . . . . . . . . 702.8.3. Teorema : ( conmutatividad ) . . . . . . . . . . . . . . . . 712.8.4. Teorema : ( Asociatividad ) . . . . . . . . . . . . . . . . . 712.8.5. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . 722.8.6. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . . 722.8.7. Observación : . . . . . . . . . . . . . . . . . . . . . . . . . 722.8.8. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . . 72

2.9. Lógica Proposicional : Resolución . . . . . . . . . . . . . 722.9.1. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 732.9.2. Ejemplo . . . . . . . . . . . . . . . . . . . . . . . . . . . 73

ÍNDICE GENERAL 4

2.9.3. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . 732.9.4. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 732.9.5. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 742.9.6. Corolario : . . . . . . . . . . . . . . . . . . . . . . . . . . 742.9.7. Ejemplo . . . . . . . . . . . . . . . . . . . . . . . . . . . . 742.9.8. Notación . . . . . . . . . . . . . . . . . . . . . . . . . . . 742.9.9. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 742.9.10. Lema : . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 742.9.11. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 752.9.12. Lema : . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 752.9.13. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 752.9.14. Lema : . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 752.9.15. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 752.9.16. Lema : . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 752.9.17. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 752.9.18. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 762.9.19. Lema : . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 762.9.20. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 762.9.21. Lema : . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 762.9.22. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 762.9.23. Regla de Resolución . . . . . . . . . . . . . . . . . . . . . 762.9.24. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 772.9.25. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . 772.9.26. Algoritmo : . . . . . . . . . . . . . . . . . . . . . . . . . . 772.9.27. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 772.9.28. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 782.9.29. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . . 782.9.30. Observación . . . . . . . . . . . . . . . . . . . . . . . . . . 782.9.31. Corolario : (Solidez ) . . . . . . . . . . . . . . . . . . . . . 782.9.32. Teorema : ( Compleción) . . . . . . . . . . . . . . . . . . 78

2.10. Semánticas y Lenguajes de Programación . . . . . . . . . 792.10.1. Necesidad de una Definición Semántica Formal . . . . . . 792.10.2. Semánticas Formales de los Lenguajes de Pro-

gramación . . . . . . . . . . . . . . . . . . . . . . . . . 812.10.2.1. Semántica Operacional . . . . . . . . . . . . . . 812.10.2.2. Semántica Axiomática . . . . . . . . . . . . . . 822.10.2.3. Semántica Declarativa . . . . . . . . . . . . . . . 82


III Lógicas 88

3. Lógica de Predicados :Fórmulas , Modelos y Tableau 893.1. Introducción . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89

3.1.1. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 89

ÍNDICE GENERAL 5

3.2. Relaciones y Predicados . . . . . . . . . . . . . . . . . . . . . . . 903.2.1. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 903.2.2. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 903.2.3. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 903.2.4. Fórmulas en Cálculo de Predicados . . . . . . . . . . . . 923.2.5. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 923.2.6. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 933.2.7. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 933.2.8. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 933.2.9. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 933.2.10. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 94

3.3. Interpretaciones . . . . . . . . . . . . . . . . . . . . . . . . . . . . 943.3.1. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 943.3.2. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 943.3.3. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 943.3.4. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 943.3.5. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . . 953.3.6. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . . 953.3.7. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 953.3.8. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 953.3.9. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 953.3.10. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 963.3.11. Ejemplo : . . . . . . . . . . . . . . . . . . . . . . . . . . . 96

3.4. Equivalencias lógicas y substitución . . . . . . . . . . . . . . . . 973.4.1. Definición : . . . . . . . . . . . . . . . . . . . . . . . . . . 973.4.2. Lo que sigue es una tabla de fórmulas válidas en cálculo

de predicados . . . . . . . . . . . . . . . . . . . . . . . . 983.4.3. Teorema : . . . . . . . . . . . . . . . . . . . . . . . . . . . 983.4.4. Observaciones : . . . . . . . . . . . . . . . . . . . . . . . . 98


Prólogo

El objetivo de este libro es dar apoyo a la docencia de elemntos básicos dela Lógica Computacional que normalmente se incluyen en los planes de estu-dio típicos de titulaciones en Programas de Ciencias de la Computación . Elconocimiento elemental que se necesita es grafos y lenguajes formales . Es re-comendable que las implementaciones de los algoritmos sean implementadas enPROLOG para reforzar el estudio de un algoritmo abstracto.

Se pretende introducir el uso de la Lógica Computacional en el aprendiza-je de la formalización del razonamiento y la modelización de situaciones quelos estudiantes encontrarán en otras asignaturas de su curriculum, tales comola especificación y verificación de sistemas computacionales, la representacióndel conocimiento o la programación declarativa. El material del libro puede sercaracterizado como extenso, elemental y riguroso: quiero cubrir profundamentemuchos temas, pero he elegido material elemental, generalmente el mínimo desubconjuntos de una lógica puede ser estudiado provechosamente. El estudianteque ha aprendido los resultados y técnicas en estos casos elementales estará bienpreparado para estudiar los sistemas más amplios en cursos mas avanzados.

El avance general en cada tema principal es: sintaxis y semántica de fór-mula, cuadros semánticos, sistemas deductivos y algoritmos. Mientras muchosmodernos libros son profundamente pesados en favor de los métodos semánticosde algoritmos, he intentado dar igual tiempo a la deducción sintáctica.

El libro desarrolla sucesivamente los siguientes aspectos de la lógica: sinta-xis y semántica, formalización y técnicas de razonamiento, leyes de equivalencialógica y cálculo lógico con tableaux. también presentamos el método de resolu-cióncomo procedimiento alternativo a los tableaux. Una característica común aestos dos métodos es que se prestan al desarrollo de herramientas de deducciónautomática. No obstante, en este libro no se ha pretendido dar énfasis al te-ma de deducción automática y se ha optado por dar mayor protagonismo a lostableaux. El motivo es que los tableaux no solamente sirven para justificas lavalidez de razonamientos correctos, sino que también permiten la construcción

6

ÍNDICE GENERAL 7

de modelos que sirven de contraejemplo para razonamientos incorrectos.

La bibliografía en el campo de la Lógica Computacional incluye bastantestextos de calidad publicados en inglés y otras lenguas de uso internacional; sinembargo, los textos publicados en español y adecuados para estudiantes de pro-gramas de Ciencias de la Computación no son tan abundantes. Por ello, confíoque este libro pueda cumplir un papel positivo para la formación matemática deestudiantes de programas de Ciencias de la Computación. Finalmente, quieroagradecer a mis estudiantes de las universidades Católica Santa María, y SanAgustín de Arequipa por la motivación a escribir este libro, que fue desarrolladoen LATEX.

Wilber Ramos Lovón, en Arequipa, noviembre 2010.

Parte I

Introducción

8

Objetivos

Este libro aspira a desarrollar una presentación básica completa a los con-ceptos que forman la base de las diferentes Lógicas, que permitirá al lector elestudio teórico de muchos conceptos importantes en ciencias de la computación,inteligencia artificial e ingeniería del software. Por ello, algunos de los temas sonde índole puramente teórico, mientras que otros tratan de establecer el puentecon las aplicaciones concretas.

La selección de los tópicos del libro están orientados a presentar los aspectosteóricos que permitan al lector comprender que , La Programación Declarativase basa en la idea de utilizar un cierto tipo de Lógica como lenguaje de progra-mación. Esto incluye tanto la programación lógica ( que usa un lenguaje clausalpara programar y el principio de resolución como mecanismo de ejecución) comola funcional (que usa el lenguaje de las funciones matemáticas y la reducción deexpresiones como mecanismo computacional).

La conexión existente entre entre la Lógica y la Ciencia de la Computación, escomparable en importancia a la relación existente entre el análisis matemático yla física. Desde el comienzo de su relación la Lógica ha jugado diferentes papelesen el campo de la Ciencia de la Computación:

1. Como una fuente de lenguajes y sistemas para el razonamiento, debido asu capacidad deductiva. Se han empleado diferentes tipos de lógicas paradescribir e implementar sistemas que razonan sobre un dominio en par-ticular, por ejemplo en los campos de la teoría de la especificación y lainteligencia artificial.La lógica temporal, una clase de lógica modal, se ha empleado para razonarsobre sistemas que incorporan el tiempo como un parámetro principal. Lalógica multimodal se ha empleado para razonar sobre sistemas concurren-tes e indeterministas. La lógica multimodal tambien es útil en el campode los lenguajes de especificación. La lógica no monótona se ha aplicado auna gran variedad de problemas que van desde la herencia de propiedadesa las bases de datos deductivas y en todas aquellas áreas en las que es ne-cesario emular razonamientos de sentido común o manejar informacionesimprecisas. La lógica difusa se ha utilizado para razonar sobre sistemas enlos que el razonamiento es incierto.

2. Como una fuente de herramientas y técnicas de análisis y fundamentación.La lógica se ha empleado como una herramienta para la representación del

9

10

conocimiento y en otras muchas áreas de la inteligencia artificial. Desdeel punto de vista de la fundamentación, la lógica se ha utilizado paraproporcionar un modelo de computo. El λ-cálculo y la reducción de λ-expresiones a formas normales, o bien la lógica de cláusulas de Horn yel principio de resolución representan visiones idealizadas de la idea decómputo. La lógica también se ha empleado para establecer una descrip-ción formal del significado (semántica) de los lenguajes de programacióny en la especificación y verificación formal de programas.

Estas son, algunas de las razones para el estudio de la lógica aparte de seruna buena vacuna contra la obsolescencia tecnolócia que siempre amenaza a losprofesionales de la computación “la lógica es particularmente importente porque es la base matemática del software” [1].

Este libro se centra, principalmente, en el estudio de las características ypropiedades fundamentales de los sistemas lógicos tradicionales: la lógica deproposiciones y la lógica de predicados. Se ha dado gran importancia a lastécnicas de formalización, y más generalmente a las técnicas de representacióndel conocimiento mediante lógica, así como a los procesos deductivos. Al tomaresta orientación se pretende que el alumno sea capaz de:

1. Tener fluidez en el uso de formalismos lógicos y la manipulación de fórmu-las. Esto es de gran interés, tanto en cuanto los lenguajes de programaciónpueden considerarse sistemas formales y sus instrucciones fórmulas.

2. Realizar demostraciones usando diferentes sistemas de deducción. Princi-palmente los llamados sistemas de decucción natural, que permiten instruiral alumno en diferentes técnicas de prueba con mayor facilidad:

a) pruebas indirectas o por deducción al absurdo

b) pruebas directas (dentro de éstas las pruebas por casos y las basadasen el teorema de la deducción).

3. Distinguir entre sintaxis y semántica y la relación existente entre ambas.

4. Conocer las propiedades formales de la lógica y sus aplicaciones.

Historia

Etapa filosófica

Silogismo :

dos Premisas (hipótesis) ⇒ Conclusión

Aristóteles (384-322 A.C.)

(1 premisa) Todo hombre es mortal(2 premisa) Sócrates es un hombre(3 conclusión ) Sócrates es mortal.

Axiomas y Teoremas (etapa no formal)

!Casi sin cambios en 2000 años!

11

12

Silogismo hipotético:

Avicena (Ibn Sina) (980-1037)

De las premisas A→ B y B → C se concluye A→ C

Desarrolló una lógica proposicional primitivaPrecursor en lógica temporal y en razonamiento inductivo

13

Tomás de Aquino (1225-1274)

La Edad Media continúa la tradición aristotélica.Máximo exponente: Tomás de Aquino Intenta compatibilizar la lógica de

Aristóteles con la fe cristiana.

0.1. Etapa matemática

Gottfried Wilhelm Leibniz (1646-1716)

Formaliza el concepto de demostración matemáticaPropone un primer sistema de inferencia: calculus ratiocinator

14

George Boole (1815-1864)

“Laws of Thought"(1854)Álgebra de Boole; Cálculo Proposicional.

Gottlob Frege (1848-1925)

“Begriffsschrift"(1879). Cálculo de predicados.

15

Bertrand Russell (1872-1970)

Alfred Whitehead (1861-1947)

Whitehead & Russell: “Principia Mathematica" (1910,1912,1913).Corpus axiomático para todas las Matemáticas

16

David Hilbert (1862-1943)

Hilbert: cálculo deductivo.Introduce la prueba formal tal como la conocemos. (1900)Dentro de sus 23 problemas: ¿son los axiomas aritméticos consistentes y

completos?

17

Alfred Tarski (1902-1983)

SemánticaDesarrolló la teoría de modelos

Jacques Herbrand (1908-1931)

Establece un método para “reducir” predicados a proposicional.Muy importante para automatizar resolución (Robinson, 1960).

18

Kurt Gödel (1906-1978)

Cálculo de predicados: completo (Gödel, 1930)Pero, el objetivo de Hilbert no se cumple: Teorema de incompletitud (Gödel,

1931)para la aritmética formal: existen fórmulas válidas que no son teoremas.

19

0.2. Etapa computacional

Alan Turing (1912-1954)

Teoría de la computabilidad: Turing, Church, Kleene.No hay algoritmo que siempre genere una prueba o indique que esta no exis-

te.

20

Tony Hoare (1934-)

Edsger W. Dijkstra (1930-2002)

Hoare, Floyd, Dijkstra. Verificación formal de programas.

21

John McCarthy (1927-)

Inteligencia Artificial McCarthy: Razonamiento de sentido común.

Robert A. Kowalski (1941-)

Kowalski: Programación Lógica.Proporciona interpretación procedural de las cláusulas de HornA. Colmerauer & P. Roussel: Prolog (1972).

José Meseguer

22

Professor of Computer Science at UIUC and leads the Formal Methods andDeclarative Languages Laboratory.

A nadie se le escapa que el crecimiento de la computación en las ultimasdécadas y su cada vez mayor influencia en la vida diaria de las personas (enalgunas partes del planeta, al menos) ha sido tremendamente espectacular. Unade las consecuencias de este desarrollo es el diseño e implementación de siste-mas más y más complejos par las más diversas tareas. En numerosas ocasionesel buen funcionamiento de dicho sistemas es crítico porque de ellos depende lavida de centenares o miles de personas (piénsese en los sistemas de control devuelo de un avión o de mantenimiento de una central nuclear) y en muchosotros las consecuencias de un error computacional, sin ser fatales, sí puedenresultar catastróficas en términos económicos (sistemas bancarios financieros).En realidad, no hace falta ir en busca de ejemplos tan grandilocuentes: senci-llamente, cuando uno escribe un programa o diseña un sistema espera que estese comporte de una manera determinada y que cumpla un propósito concreto.A partir de cierto grado de complejidad de un proyecto, la ausencia de errorespasa a ser un objetivo inalcanzable; sin embargo, ello no debería ser óbice paraintentar conseguir que su número sea lo más reducido posible. En este sentido,resulta especialmente interesante el uso de lenguajes de especificación, forma-lismos que por un lado sean flexibles y potentes para permitir manejar diseñosde complejidad elevada, pero que por otro lado tengan un significado matemáti-co preciso. Idealmente, dichos lenguajes deberían imponer una cierta disciplinametodológica de forma que se redujera el numero de errores durante la etapade codificación, mientras que disponer de una semántica matemática precisadebería servir para, aun cuando no se pueda asegurar que el sistema esté librede errores, garantizar que al menos se cumplan las propiedades que a nosotrosnos interesan. Uno de tales mecanismos es la lógica de reescritura presentadapor José Meseguer a comienzos de los años noventa (Meseguer, 1992). En el que

23

se define la teoría de modelos de la lógica y se presenta un cálculo deductivocorrecto y completo. Que vienen a ser la base de un lenguaje declarativo deespecificación y programación, llamado Maude (Clavel et al., 1996, 2004a).

Parte II

Los Fundamentos

24

Capítulo 1

Una Panorámica de laProgramación Declarativa

1.1. Computadores y Lenguajes de Progra-mación

La mayoría de los computadores modernos presentan una organización ba-sada en el llamado modelo de Von Neumann1.

Los lenguajes imperativos o convencionales son una abstracción de alto nivelde la estructura de la máquina para la que se han desarrollado y que muchosde sus defectos e imperfecciones provienen de esa estrecha relación. De hecho,los distintos recursos expresivos proporcionados por tales lenguajes pueden ver-se como abstracciones de las operaciones elementales de los componentes de lamáquina de Von Neumann. Así pues, los lenguajes de programación imperati-vos, independientemente del número de niveles software existentes entre ellos,son en esencia una extención del lenguaje de máquina.La instrucción de asignación resulta ser representativa del cuello de botella deVon Neumann y nos obliga a pensar en términos de trasiego de información en-tre celdas de memoria. Más todavía, Backus ha hecho notar que la instrucciónde asignación separa la programación en dos mundos. El primero comprendela parte derecha de las instrucciones de asignación. Este es un mundo de ex-presiones, con propiedades algebraicas muy útiles en el que se realiza la mayorparte del cómputo. El segundo es el mundo de las instruciones, en el que la pro-pia instrución de asignación puede considerarse una instrucción primitiva en laque se basan las demás. Este es un mundo desordenado, con pocas propiedadesmatemáticas útiles [2].

1

Propuesta por el matemático J. Von Neumann, a mediados de los años cua-renta.

25

CAPÍTULO 1. UNA PANORÁMICA DE LA PROGRAMACIÓN DECLARATIVA26

Se pueden distinguir dos aspectos fundamentales en las tareas de programa-ción :

Aspectos Lógicos: Esto es, ¿Qué debe computarse?. Esta es la cuestiónesencial y, de hecho, es la que motiva el uso de un ordenador como mediopara resolver un determinado problema.

Aspectos de Control, entre los que podemos distinguir:

• Organización de la secuencia de computos en pequeños pasos.• Gestión de la memoria durante la computación.

Dado que dichos aspectos lógicos y de control se refieren a componentes clara-mente distintos e independientes de las tareas de programación (especificacióndel problema e implementación del programa que lo resuelve, respectivamente),parece deseable que los lenguajes de programación nos permitan mantener lasdistancias entre ambos, sin necesidad de que las cuestiones implicadas en las ta-reas de especificación e implementación interfieran entre si. De acuerdo a esto,se pueden hacer algunas críticas al uso de los lenguajes imperativos.

1. La presencia de instrucciones de control de flujo (sentencias if, while, for,etc.) y las operaciones de gestión (distinción entre declaración y definiciónde una estructura o variable del programa; necesidad de reserva y libe-ración explícita de la memoria; uso de punteros), oscurecen el contenidológico (puramente descriptivo) del programa.

2. En el ambito matemático, un símbolo de variable siempre denota el mismoobjeto, cualquiera que sea la ocurrencia de ese símbolo que consideremos.Sin embargo, la operación de asignación (por ejemplo; x:=x+1) utiliza lasvariables de modo matematicamente impuro.Este uso no matemático de las variables, unido al hecho de que la instruc-ción de asignación es sensible a la historia de la computación, dificultael razonamiento sobre las propiedades de los programas. En general, noes suficiente con conocer el significado de los constituyentes del programapara establecer su significado sino que en realidad, ese significado dependedel contexto donde aparecen dichos constituyentes, y de la historia previade la computación , que permiten la introducción de efectos laterales (esdecir, el significado del del programa no podrá entenderse en terminos decomposicionalidad).

3. Dejar las cuestiones de control al programador no parece lo más indicado.Por ejemplo, un programa escrito en Pascal para una máquina de un únicoprocesador desaprovechará los recursos ofrecidos por una máquina conmuchos procesadores. A menudo será dificil para el compilador generar uncódigo que aproveche al máximo las características de la máquina objeto,puesto que parte del control (secuencial) estará ya especificado por elprogramador en el texto del programa.2

2Ver ejemplo en [2], pg. 7.


Hemos puesto de manifiesto los puntos débiles de los lenguajes imperativos, quejustifican el estudio de otros paradigmas de programación.

1.2. Programación Declarativa

La programación declarativa (también llamada programación inferencial)puede entenderse como un estilo de programación en el que el programadorpone su total atención en especificar qué debe computarse y no en cómo debenrealizarse los computos. En este paradigma de programación, de acuerdo conKowalski 3, un programa=lógica+control, y la tarea de programar consiste encentrar la atención en la lógica dejando de lado el control, que se asume auto-mático, al sistema. El componente lógico determina el significado del programamientras que el componente de control solamente afecta a su eficiencia. Estadistinción tiene la ventaja de que la eficiencia de un programa puede mejorarsemodificando el componente de control sin tener que modificar la lógica del algo-ritmo (del que el programa es una representación posible en la máquina). Conmás presición, la característica fundamental de la programación declarativa es eluso de la lógica como lenguaje de programación, lo cual puede conceptualizarsecomo sigue:

Un programa es una teoría formal en una cierta lógica, esto es, un conjuntode fórmulas lógicas que resultan ser la especificación del problema que sepretende resolver, y

la computación se entiende como una forma de inferencia o deducción endicha lógica.

Los requisitos que debe cumplir la lógica empleada son :

Disponer de un lenguaje que sea suficientemente expresivo para cubrir uncampo de aplicación interesante;

Disponer de una semántica operacional, esto es, un mecanismo de computoque permita ejecutar los programas ;

Disponer de una semántica declarativa que permita dar un significado alos programas de forma independiente a su posible ejecución; y

Resultados de corrección y completitud que aseguren que lo que se compu-ta coincide con aquello que es considerado como verdadero (de acuerdo conla noción de verdad que sirve de base a la semántica declarativa).

Desde el punto de vista del soporte a la declaratividad, el tercero de los requisitoses, tal vez, el más importante, ya que es el que permite especificar qué estamoscomputando. Concretamente, la semántica declarativa especifica el significadode los objetos sintácticos del lenguaje por medio de su traducción en elementos y

3ver quien es


estructuras de un dominio (generalmente matemático) conocido. Según la clasede lógica4que empleemos como fundamento del lenguaje declarativo obtenemoslos diferentes estilos y características para esta clase de lenguajes.La siguiente tabla los estilos de programación declarativa y características he-redadas de la lógica que la fundamenta:

Clase de Lógica Estilo/CaracterísticaEcuacional FuncionalClausal Relacional

Heterogenea TiposGéneros Ordenados Herencia

Temporal Concurrencia

1.3. Programación Lógica - ProgramaciónFuncional

La programación lógica se basa en fragmentos de la lógica de predicados,siendo el más popular la lógica de cláusulas de Horn (HCL, del inglés Hornclause logic), que pueden emplearse como base para un lenguaje de programa-ción al poseer una semántica operacional susceptible de una implementacióneficiente, como es el caso de la resolución SLD. Como semántica declarativa seutiliza una semántica por teoría de modelos que toma como dominio de interpre-tación un universo de discurso puramente sintáctico: el universo de Herbrand. Laresolución SLD5 es un método de prueba por refutación que emplea el algoritmode unificación como mecanismo de base y permite la extracción de respuestas (es decir, el enlace de un valor a una variable lógica). La resolución SLD es unmétodo de prueba correcto y completo para la lógica HCL.

Los lenguajes funcionales están enraizados en el concepto de función (ma-temática) y su definición mediante ecuaciones (generalmente recursivas), queconstituyen el programa. Desde el punto de vista computacional, la progra-mación funcional se centra en la evaluación de expresiones (funcionales) paraobtener un valor. En programación funcional la descripción de dominios condu-ce a la idea de tipo de datos. Los tipos de datos se introducen en programaciónpara evitar o detectar errores y ayudar a definir estruturas de datos. Los len-guajes funcionales modernos son lenguajes fuertemente basados en tipos, ya querealizan una comprobación de las expresiones que aparecen en el programa paraasegurarse de que no se producirán errores durante la ejecución del mismo por

4Algunas de estas clases son restricciones de la lógica de primer orden, como la lógicaclausal o la lógica ecuacional.

5Las siglas SLD hacen mención a las iniciales inglesas de “resolución lineal con funciónde selección para programas definidos”. Esta estrategia también se ha denominado resoluciónLUSH, aquí las siglas hacen referencia a “Linear resolution with Unrestricted Selection fuctionfor Horn clauses”. Por otra parte, Kowalski la ha denominado inferencia analítica (top-downinference).


incompatibilidades de tipo. No obstante, suelen incorporar también un mecanis-mo automático de inferencia de tipos que libera al programador de la necesidadde declarar éstos ya que son deducidos por el intérprete.

Lo que caracteriza a una función (matemática), es que a cada elemento desu dominio le corresponde un único elemento del rango; en otras palabras, elresultado (salida) de aplicar una función sobre sus argumentos viene determi-nado exclusivamente por el valor de éstos (su entrada). Esta propiedad de lasfunciones (matemáticas) se denomina transparencia referencial. Debido aque los programas en los lenguajes imperativos mantienen un estado interno delcomputo, que es modificado durante la ejecución de la secuencia de instruccio-nes, las construcciones funcionales de estos lenguajes pueden presentar efectoslaterales, incumpliendo la propiedad de transparencia referencial y no deno-tando, por consiguiente, verdaderas funciones (matemáticas). La transparenciareferencial permite el estilo de la programación funcional basado en el razo-namiento ecuacional (la sustitución de “iguales por “iguales”, es decir, de unaexpresión por otra equivalente) y los computos deterministas. Desde el puntode vista computacional, otra propiedad de las funciones (matemáticas) es sucapacidad para ser compuestas. La compocición de funciones es la técnica porexcelencia de la programación funcional, que permite la construcción de progra-mas mediante el empleo de funciones primitivas o previamente definidas por elusuario. La composición de funciones refuerza la modularidad de los programas.

Una de las características de los lenguajes funcionales que va más alla dela mera composición de funciones es el empleo de las mismas como “ciudada-nos de primera clase” dentro del lenguaje, de forma que las funciones puedanalmacenarse en estructuras de datos, pasarse como un argumento a otras fun-ciones y devolverse como resultado. Agrupamos todas estas caraterísticas bajola denominación de orden superior .

La ejecución de un programa consiste en la evaluación de una expresióninicial de acuerdo con las ecuaciones de definición de las funciones y algúnmecanismo de reducción. La reducción es un proceso por el cual, mediante unasecuencia de pasos, transformamos la expresión inicial, compuesta de símbolosde función y de símbolos constructores de datos, en un valor (de su tipo), esdecir, una expresión que solo contiene ocurrencias de símbolos constructores.El valor obtenido se considera el resultado de la evaluación. La secuencia depasos dada en el proceso de reducción depende de la estrategia de reducciónempleada. Destacan dos estrategias de reducción o modos de evaluación, ladenominada impaciente y la peresoza6. Una estrategia impaciente no evalúa lafunción hasta haber evaluado completamente sus argumentos mientras que unaperezosa evalúa los argumentos solo si su valor es necesario para el computode dicha función, intentando evitar cálculos innecesarios. Por ejemplo, dada lafunción: doble x = x + x un paso de evaluación impaciente a partir de laexpresión: doble 4 + 8 produciría: doble 12 , mientras que, tras un paso de

6En algunos contextos como el λ-cálculo, la estrategia de reducción impaciente (eager) seidentifica con el orden de reducción aplicativo, mientras que la perezosa (lazy) con el orden dereducción normal. En los lenguajes imperativos, estas estrategias corresponderían básicamenteal paso de parámetros por valor y por nombre, respectivamente.


reducción perezosa, obtendríamos : (4 + 8) + (4 + 8).Si bien la estrategia impaciente es más facil de implementar en los compu-

tadores con arquitecturas convencionales7 puede conducir a secuencias de re-ducción que no terminan en situaciones en las que una evaluación perezosa escapaz de computar un valor. Por ejemplo, la evaluación de la expresión: esCeroinfinito , no termina bajo una estrategia de evaluación impaciente, mientrasque el resultado es False usando una estrategia perezosa. De hecho, de estasdos estrategias sola la perezosa es justa (fair), en el sentido de garantizar lacomputación del valor de cada expresión de entrada, si éste existe.

Este hecho, junto con algunas facilidades de programación (la evaluación pe-rezosa libera al programador de la preocupación por el orden de evaluación de lasexpresiones, un tema recurrente cuando el programador quiere ganar eficienciaes su preocupación por no evaluar aquello que no es absolutamente necesario) yventajas expresivas que proporciona ( la habilidad de computar con estructurasde datos infinitas), ha hecho que la posibilidad de utilizar un modelo de evalua-ción peresoza sea muy apreciada en los lenguajes funcionales modernos. Muchosde los primeros lenguajes funcionales, como Lisp (puro), fueron implementadosempleando un modo de evaluación impaciente por razones ya comentadas. Sinembargo, desde que existe técnicas eficientes de implementación de la reducciónen grafos, los lenguajes funcionales como Haskell utilizan modos de evaluaciónperezosa. En este tipo de implementación, la expresión (4 + 8) del ejemplo an-terior se evaluaría una vez, ya que sus dos apariciones dentro de la expresión(4 + 8) + (4 + 8) se ubican en un único nodo del grafo.

Como puede apreciarse los lenguajes de programación funcional son muyricos en cuanto a las facilidades que ofrecen8 . La siguiente tabla resume lascaracterísticas de los lenguajes funcionales en comparación con los lenguajeslógicos.

7La estrategia de evaluación impaciente puede implementarse utilizasndo las técnicas depaso de parámetros por valor desarrolladas para la compilación de los lenguajes imperativos.

8Algunas de las ventajas que hemos discutido en esta sección asociadas a los lenguajesfuncionales han sido transferidas a lenguajes orientados a objetos. Se ha acuñado el acrónimoHOT ( del inglés High Order and strongly Typed) para hacer referencia a los lenguajes deprogramación que reúnen estas características. Puede decirse que los lenguajes orientados aobjetos como Java son HOT, si bien el polimorfismo y el orden superior se obtienen en estelenguaje de manera oscura y un tanto imperfecta a través del mecanismo de la herencia.


Programación Lógica Programación FuncionalPrograma: Programa:

Cláusulas que definen relaciones Ecuaciones que definen funcionesSemántica Operacional Semántica OperacionalResolución SLD (unificación) Reducción (ajuste de patrones)Semántica Declarativa Semántica Declarativa

Teoría de modelos (Modelo mínimo) Algebraica(Modelo inicial) / DenotacionalPrimer Orden Orden Superior

Uso múltiple de un procedimiento Uso único de cada funciónIndeterminismo Determinismo

E/S E/SAdireccional Direccional y transparencia referencial

Variables Lógicas Sin Variables LógicasSin Tipos Tipos y Polimorfismo

Datos parcialmente especificados Datos completamente definidosNo estructuras infinitas Estructuras potencialmente infinitasNo evaluación perezosa Evaluación perezosa

Evitaremos hablar de los formalismos que sustentan esta clase de lenguajes,debido a que no hay un concenso unánime (como en el caso de la programaciónlógica) en la utilización de un determinado tipo de lógica. Pueden distinguirsetres diferentes aproximaciones: la ecuacional, la algebraica y la funcional clásica.Sin embargo, es de destacar que la orientación que fundamenta la programaciónfuncional en la lógica ecuacional y en los sistemas de reescrirtura tiene la ventaja,respecto a la orientación clásica, de que puede establecerse una correspondenciamás sencilla con el formalismo que sustenta la programación lógica9 .

1.4. Comparación con los Lenguajes Impe-rativos y Áreas de Aplicación

El objetivo de esta sección, es que el lector sea conciente de que tanto laprogramación declarativa como la imperativa presentan ventajas que puedenser muy útiles en las áreas de aplicación apropiadas. En este punto es conve-niente remarcar que ningún lenguaje, hasta la fecha, se ha adaptado a cualquiertipo de aplicación. Así por ejemplo, el lenguaje PL/I, primer intento de lengua-je “totalitario” (auspiciado por IBM) que pretendia aunar las características deCOBOL (un lenguaje para el desarrollo de aplicaciones de gestión en la empre-sa) y FORTRAN (un lenguaje diseñado para el cálculo numérico) solo tuvo unéxito modesto en los años 70, ya que carecía de una visión semántica uniforme y,finalmente, perdía las ventajas especificas de los lenguajes originales. Algo pare-cido sucedió con el desarrollo del lenguaje ADA, auspiciado por el departamentode defensa de los EEUU [2].

9Esta ventaja es apreciable a la hora de integrar ambos paradigmas de programación.


Realizaremos la comparación entre los lenguajes declarativos y los impera-tivos, estudiando una serie de atributos y criterios que se han utilizado paramedir la calidad de los lenguajes de programación y comentando en qué medidase ajusta cada clase de lenguaje a estos criterios.

1.4.1. Diseño del Lenguaje y Escritura de Programas

Desde esta perspectiva pueden citarse las siguientes características útilespara un lenguaje:

1. Sintaxis Sencilla. El programador desea que la sintaxis de un lenguaje deprogramación sea sencilla, ya que ésta facilita el aprendizaje y la escriturade aplicaciones. Los lenguajes declarativos poseen esta caracte-rística en alto grado, mientras que la sintaxis de los lenguajes impera-tivos suele ser muy compleja. Esta situación se agrava particularmente enlos lenguajes orientados a objetos a los que se aúna cantidad inmanejablede librerías “estándares” que conducen a un prolongado aprendizaje.

2. Modularidad y Compilación Separada. Estas características facilitan la es-tructuración de los programas, la división del trabajo y la depuración delos programas durante la fase de desarrollo. Respecto a este último punto,un diseño modular aisla y localiza los errores, que solo podrán provenirde los módulos actualmente en desarrollo y no de los ya depurados y va-lidados. Por otra parte, la posibilidad de efectuar complilación separadaes un factor de ahorro de tiempo ya que no será necesario complilar to-dos los módulos cada vez que se introduzcan modificaciones. La mayoriade los lenguajes imperativos proporcionan facilidades para la construcciónde módulos y la compilación separada. Los lenguajes declarativos,si bien permiten undesarrollo modular dee las aplicaciones,no suelen presentar herramientas para la compilación separa-da, máxime cuando muchos de ellos nacieron como lenguajesinterpretados.

3. Mecanismos de Reutilización del Software . Para eliminar la repetición detrabajo, un lenguaje también debe de suministrar mecanismos para reutili-zar el software ya desarrollado y que se adecúa al problema a resolver. Estees un punto ligado al anterior. Los lenguajes imperativos, al poseer meca-nismos más evolucionados para la modularidad y la compilación separada,han ofrecido mejores condiciones para la reutilización del software. El usode la modularidad y la compilación separada ha permitido la creaciónde potentes bibliotecas que pueden considerarse extenciones del lenguajepara el que se han escrito y que facilitan la tarea de la programación.Esta potencialidad se ha desarrollado hasta el extremo en los lenguajesorientados a objetos. Por su parte, los lenguajes declarativos sue-len realizar esta funciónmediante, por ejemplo la inclusiónde “preámbulos de funciones”, un mecanismo más ineficiente y


rudimentario. También, en la actualidad se está investigando como au-mentar la reutilización del software en los lenguajes declarativos medianteel suministro de bibliotecasde plantillas genéricas y simples ( cuyo sig-nificado declarativo fuese, sin duda, el esperado) que posteriormente seoptimizarían utilizando uan técnica de transformación automática de pro-gramas para producir un código más eficiente10 .

4. Facilidades de Soporte al Proceso de Análisis. Los lenguajes declara-tivos pueden considerarse lenguajes de especificación. En estesentido serían muy adecuados en las fases de análisis de unaaplicación y su rápido prototipado. Sin embargo, el relativo bajonivel de los lenguajes imperativos hace que sus construcciones estén ale-jadas del nivel de abstracción que requiere el análisis de un problema, porlo que se hace imprescindible el uso de algún tipo de pseudocódigo para laconfección de un algoritmo, siguiendo algún tipo de técnica de diseño (esdecir, diseño descendente - topdown), que después es traducido al lenguajeelegido, en la fase de implementación. La dificultad que presentan estoslenguajes ha hecho que surjan diversas herramientas de ayuda al análisisy diseño.

5. Entornos de Programación. Aunque no está ligado al diseño del lenguajeen sí y aunque pueda parecer secundario éste es un factor muy importante,ya que un buen entorno de programación puede hacer que sea más faciltrabajar con un lenguaje técnicamente poco evolucioinado que con unoevolucionado, pero que ofrece poco soporte externo.Un buen entorno de programación debe ofrecer editores especiales quefaciliten la escritura de programas, depuradores y, en general, utilidades deayuda para la programación que permitan modificar y mantener grandesaplicaciones con multiples versiones. Si bien la mayoria de los lenguajesimperativos de uso en la actualidad cuentan con potentes entornos deprogramación (muchos de ellos visuales), los lenguajes declarativostienen aquí uno de sus puntos débiles. Una explicación a este hechoes que los lenguajes declarativos se han desarrollado y usado en ambientesuniversitarios y en grupos de investigación en los que estas facilidades nohan sido suficientemente valoradas. Esta es una situación que cambiaráconforme las técnicas que introduce la programación declarativa sean másapreciadas en sectores industriales.

Verificación de Programas

La fiabilidad de los programas es un criterio central para medir la calidad deldiseño de un lenguaje de programación. Hay diversas técnicas para verificar que

10La transformación automática de programas es un método para derivar programas correc-tos y eficientes partiendo de una especificación ingenua y más ineficiente del problema. Estoes, dado un programa P, se trata de generar un programa P’ que resuleve el mismo problemay equivale semánticamente a P, pero que goza de mejor comportamiento respecto a ciertocriterio de evaluación.


un programa realiza correctamente la función para la que fue creado. Nosotroscomentaremos tanto las técnicas formales como las informales y el grado deadaptación de los lenguajes a dichas técnicas:

1. Verificación de la Corrección. Consiste en comprobar si el programa secomporta de acuerdo a su significado esperado, es decir a su semántica.Otra fórmula alternativa de presentar este problema sería: Dado un progra-ma P y su especificación S ¿conputan P y S la misma función? Los len-guajes declarativos, por poseer definiciones semánticas sen-cillas y estar basados en sólidos fundamentos que permitenaplicar los métodos formales de las matemáticas, pueden res-ponder con relativa sencillez a este tipo de preguntas. No esel caso de los lenguajes imperativos, que poseen definiciones semánticasmuy complejas y que, por consiguiente, están peor adaptados a este tipode comprobaciones formales.

2. Terminación. Un programa no solamente debe presentar el comportamien-to deseado, sino que además debe terminar bajo cualquier circunstanciaconcebible. Por identicas razones que en el caso anterior, los lenguajesdeclarativos están adaptados para realizar este tipo de prue-bas, motivo por el cuál existe una amplia literatura sobre terminación deprogramas lógicos y funcionales.

3. Depuración de Programas. Si bien la comprobación del correcto funciona-miento de un programa mediante baterías de pruebas, en las que se utilizanconjuntos de datos concretos, no asegura un programa libre de errores, és-te es un método muy socorrido por los programadores, pero solo aseguraque el programa es correcto para la baterá de pruebas realizada. Así pues,si se desea un alto grado de certeza, esta batería debe ser significativa,realizando un estudio exhaustivo de casos, lo que alrga el tiempo de desa-rrollo del programa. Si para unos ciertos datos de entrada se observa unasalida inesperada o se detecta un error, el programa deberá a proceder ala depuración del programa. Para ayudar en esta tarea, el lenguaje debesuministrar mecanismos que permitan la detección rápida de errores entiempo de compilación (que de apareceer entiempo de ejecución sería másdifíciles de depurar) y herramientas de depuración de errores en tiempode ejecución (debugger). Pero también es es necesario que el lenguaje sealegible para que, en caso de que los errores aparezcan en tiempo de eje-cución, no sea muy complicado llegar a comprender el código fuente yasí identificar rápidamente la fuente del error. Los lenguajes decla-rativos poseen una buena legibilidad pero no ofrecen buenasherramientas de depuración (la depuración de errores se concreta enla realización de tediosas trazas de ejecución). Sin embargo, los lenguajesimperativos poseen herramientas de depuración muy potentes, aunque sulegibilidad suele ser peor.


1.4.2. MantenimientoMuchos estudios han mostrado que el mayor coste en un programa, que se

usa durante un periodo de varios años, es el coste de mantenimiento. El man-tenimiento incluye la reparación de los errores descubiertos despues de que elprograma se ha puesto en uso, así como la implementación de cambios necesa-rios para satisfacer nuevas necesisdades. Para realizar estas tareas, el lenguajedebería de poseer:

1. Facilidad de uso y Lectura. Esto es necesario para que no sea muy compli-cado llegar a comprender el texto de programa y encontrar rápidamentelos errores, en caso de que éstos se produzcan. También, si hay que exten-der el programa, un programador que no conozca la aplicación (o inclusoel lenguaje) se beneficiará de estas propiedades.

2. Modularidad y Compilación Separada. Esto es necesario para que los erro-res estén localizados y así facilitar las modificaciones. Nuevamente, la po-sibilidad de realizar compilación separada evita tener que compilar todoslos módulos y ahorra gran cantidad de tiempo de desarrollo.

El grado en el que los lenguajes declarativos y los imperativos se adaptan a estaspropiedades ya fue discutido en el punto (1.4.1).

1.4.3. Coste y EficienciaEste aspecto es uno de los más importantes a la hora de evaluar un lenguaje

de programación. Existen muchos factores para los que se puede aplicar uncriterio de coste, sin embargo nos centraremos en dos de ellos:

1. Coste de Ejecución. Históricamente se ha dado gran importancia al cos-te de ejecución como medida de la eficiencia de los programas. El costede ejecución es de primera importancia en aplicaciones que se ejecutanrepetidamente. Uno de los puntos débiles de los lenguajes de-clarativos es que suelen ser menos eficientes que los impera-tivos. La causa radica en la dificultad de implementar, en máquinas dearquitecturas convencionales, las operaciones de unificación y empareja-miento, así como los mecanismos de búsqueda de soluciones que utilizanestos lenguajes. Por contra, los lenguajes imperativos son eficientes, ya quesu diseño es reflejo del modelo de Von Neumann de computación, en elque se basa la arquitectura de los computadores actuales. No obstante, enlos últimos años, se han desarrollado como ya dijimos implementacionesmuy eficientes de Haskell o Prolog, que igualan y en ocasiones superana la de lenguajes más populares como Java, cuya eficiencia no suele sercuestionada debido a sus innegables ventajas en otros frentes.

2. Coste de Desarrollo. Comprende los costes asociados a las fases de aná-lisis, programación y verificación de un programa. Es un criterio muy atener en cuenta, ya que el coste de hora de programar es muy alto frente


al de hora de UCP11 . Las estadísticas indican que, para ciertotipo de aplicaciones, los costes de desarrollo son muy bajoscuando se utilizan lenguajes declarativos y , por el contrario, loscostes de utilizar lenguajes imperativos suelen ser altos. Habitualmente,en un lenguaje declarativo el número de líneas requerido para implemen-tar un programa que resuelve un problema es una fracción del requeridocuando se usa un lenguaje imperativo (la relación entre el número de lí-neas escritas en Prolog y el de escritas en C es 1/10 en aplicaciones quedesarrollan sistemas expertos y de 1/8 para aplicaciones que desarrollancompiladores). Teniendo en cuenta que el número de líneas producidas alaño por un programador profesional es una constante, independientemen-te del lenguaje que utilice, la reducción en los costes de desarrollo cuandose emplean lenguajes declarativos puede ser considerable.

Las discusión anterior revela que un lenguaje de programación nunca es buenopara todas las tareas. Por consiguiente, cada lenguaje tiene su dominio de apli-cación para una discusión sobre algunos lenguajes y sus dominios de aplicacióntrasdicionales: computación simbólica, científica, gestión, sistemas, etc.

A pesar de ser un área de trabajo relativamente nueva, en términos del tiem-po necesario para el desarrollo y la consolidación de un área de conocimiento,la programación declarativa ha encontrado una gran variedad de aplicaciones,enumeramos algunas de éstas :

1. Procesamiento del Lenguaje Natural

2. Representación del Conocimiento

3. Química y Biología Molecular

4. Desarrollo de Sistemas de Producción y Sistemas Expertos

5. Prototipado de Aplicaciones

6. Bases de Datos Decuctivas

7. Servidores y Buceadores de Información Inteligentes

8. Diseño de Sistemas VLSI, herramientas de soporte al desarrollo del soft-ware

En general, la programación declarativa se ha aplicado en todos los campos de lacomputación simbólica, la inteligencia artificial y la informática teórica (Teoríade Tipos). Algunos lenguajes como Prolog, λ-Prolog, Lisp (puro), ML, Haskell,Curry y Toy12 son lenguajes declarativos de proposito general, mientras quelas hojas de cálculo y el lenguaje SQL (Structured Query Language) puedenconsiderarse lenguajes declarativos para dominios de aplicación especificos. Las

11Unidad Central de Proceso12Curry y Toy son lenguajes, todavía en desarrollo, que integran las características de los

lenguajes lógicos y funcionles.


hojas de cáculo realizan tareas de cómputo mediante la definición de expresionesmatemáticas. El lenguaje SQL es un lenguaje de consulta a bases de datos queutiliza las construcciones del álgebra relacional.

También es impórtante mencionar algunas características que surgieron conlos lenguajes declarativos y que han influido posteriormente en la concepción deotros lenguajes. Por ejemplo, la precompilación de Prolog producía un códigointermedio portable comparable a la idea de los bytecode de Java; por otrolado, Java hereda también la gestión dinámica de la memoria heap con garbagecollection de lenguajes funcionales como LISP (que no tienen otros lenguajesimperativos como C++.

1.5. Lista de Ejercicios1. ¿Cuáles son los puntos débiles de los lenguajes imperativos?

2. ¿En qué clase de lógica se fundamenta se fundamentan los lenguajes fun-cionales?

3. ¿A que se denomina transparencia referencial?

4. Explique los procesos de reducción o modos de evaluación; impaciente yperezosa.

5. ¿Qué es un programa en el contexto de la programación declarativa?

6. Indique cuál de las siguientes características no es de la programaciónimperativa:

a) Programa = transcripción de un algoritmo.

b) Instrucciones = órdenes a la máquina.

c) Modelo Computacional = máquina de inferencias lógicas.

d) Variables del Programa = referencias a memoria

7. Enumere las principales características que se asocian con un lenguaje deprogramación declarativo.

8. ¿Cuáles de los siguientes lenguajes podría considerarse tanto un lengua-je de especificación ejecutable como un lenguaje de programción de altonivel?

C, C++ , Java , Haskell, Pascal, Prolog, Maude

9. Señale cuál de las siguientes ideas no pertenecen al estilo de la programa-ción declarativa:

a) Programa = lógica + control.


b) Programación = demostración de teoremas + técnicas de extracciónde respuestas.

c) Programación = lenguaje de la lógica de primer orden como notaciónpara los programas e inferencia lógica como mecanismo de compu-tación.

d) Programación = algoritmo + estructura de datos.

10. Indique cuál de las siguientes ideas no se relacionan con estilo de la pro-gramación declarativa:

a) Programa = teoría formal que especifica un problema.

b) Semántica Operacional = deducción o inferencia lógica.

c) Programa = secuencia de ordenes que operan sobre los estados de lamáquiana.

d) Programa = lógica + control.

Capítulo 2

Sistemas Formales yLógica de Proposiciones

2.1. Sistemas Formales

La palabra formal se usa para referirnos a esa situación en la que se empleasímbolos cuyo comportamiento y propiedades están completamente determina-dos por un conjunto dado de reglas.

2.1.1. Observación:Lo que sigue son algunas de las propiedades deseables de los sistemas for-

males:

Consistencia

Un Sistema Formal es consistente cuando de él no se desprenden contra-dicciones, esto es, es imposible demostrar una fórmula y la negación deesa fórmula.

Corrección

Un Sistema Formal es correcto si toda fórmula demostrable sin premisas,es válida: Todo lo demostrable es verdadero.

Completitud

Un Sistema Formal es completo si toda fórmula que es válida, según lanoción de verdad, es demostrable sin premisas: Todo lo que es verdaderose puede demostrar .

Decidibilidad

Un Sistema Formal es decidible si existe un procedimiento finito paracomprobar si una fórmula es o no válida.

39

CAPÍTULO 2. SISTEMAS FORMALES Y LÓGICA DE PROPOSICIONES 40

2.2. Lógica de Proposiciones: Sintaxis

En ciencia de la computación, el término expresión es usado para denotarla construccion de valores complejos a partir de valores elementales, en lógicaproposicional, el término fórmula proposicional o simplemente fórmula es usadoen su lugar.

Las fórmulas sintácticamente correctas1 son descritas por gramaticas libresde contexto. En el lógica proposicional los símbolos terminales: son los operado-res booleanos y los símbolos de un conjunto P llamados letras proposicionaleso proposiciones atómicas. Las proposiciones atómicas son denotadas por letrasminúsculas en el conjunto {p, q, r,· · ·} posiblemente con subíndices.

2.2.1. Definición: (Sistema Formal)Un Sistema Formal S es un modelo de razonamiento matemático en el que

se distinguen los siguientes componentes:

1. Sintaxis.

a) Lenguaje Formal: Conjunto de símbolos y fórmulas sintácticamentecorrectas. Para definir un lenguaje formal se necesita:

1) Un vocabulario o alfabeto: Un conjunto numerable de letras ysímbolos a utilizar en las construcciones de S.

2) Reglas: que establezcan qué cadenas de signos son fórmulas bienformadas (fbf) en S.

b) Cálculo Deductivo: Conjunto de Reglas que permiten obtener fórmu-las nuevas atendiendo solo a aspectos sintácticos de los símbolos. Uncáculo deductivo queda definido especificando:

1) Un conjunto (posiblemente vacío) de fórmulas bien formadas deS que van a utilizarce como axiomas.

2) Un conjunto finito de reglas de inferencia.3) Un concepto de dedución (demostración), formalizado como un

conjunto de reglas para construir las estructuras deductivas co-rrectas, junto con las condiciones que debe reunir una deduciónpara dar como resultado un teorema de S.

2. Semántica.

La semántica estudia la descripción de significado a los smbolos y fórmulasde los lenguajes formales. Para ello se introduce el concepto de interpre-tación que, habitualmente, consiste en una serie de reglas precisas quepermiten asignar objetos de un dominio (no necesariamente matemático)a ciertas expresiones del lenguaje formal. Esto se acompaña de una no-ción de valoración y un conjunto de reglas de valoración que hace posibleidentificar cuándo una fórmula es verdadera en una interpretación.

1Fórmulas bien formadas (fbf)


2.2.2. Operadores BooleanosUn tipo de dato consiste de un conjunto de valores y un conjunto de ope-

radores predefinidos sobre estos valores. Por ejemplo (Z,+,−, ∗, div,mod ) . Elcálculo proposicional se refiere a las expresiones sobre el tipo booleano que tie-ne dos valores indicados T y F. Puesto que el conjunto de valores es finito, elnúmero de posibles operadores de n-plazas es finito para cada n. Hay 22n

opera-dores booleanos de n-plazas op(x1, x2, · · · , xn). El siguiente cuadro muestra losposibles operadores de una plaza:

x o1 o2 o3 o4

T T T F FF T F T F

De los cuatro operadores de una plaza tres son triviales : o1y o4 son operado-res constantes y 02 es el operador identidad. Solo es no trivial o3 que es llamadonegación, que es denotado con ¬ y que leeremos como not. Negación apareceen todas las aplicaciones de la lógica: en electrónica, la compuerta not se utili-za para transformar una señal de entre dos niveles de voltaje discreto, y en laprogramación, el operador not se utiliza explicitamente en el operador diferente(denotada con: / =, <>) , e implícitamente en la sentencia If-Then-Else.

El siguiente cuadro muestra los posibles 222= 16 operadores de 2 plazas:

x1 x2 o1 o2 o3 o4 o5 o6 o7 o8

T T T T T T T T T TT F T T T T F F F FF T T T F F T T F FF F T F T F T F T Fx1 x2 o9 o10 o11 o12 o13 o14 o15 o16

T T F F F F F F F FT F T T T T F F F FF T T T F F T T F FF F T F T F T F T F

Varios de los operadores son triviales: o1 y o16 son constantes; o4 y o6 sonlos operadores de proyección, es decir, su valor se determina solo por el valor deun operando; o11 y o13 son las negaciones de los operadores de proyección. Losoperadores interesantes y sus negaciones son mostradas en la siguiente tabla:

op nombre símbolo op nombre símbolo02 disyunción ∨ o15 nor ↓o8 conjunción ∧ o9 nand ↑o5 implicación → o12

o3 implicación reversa ← o14

o7 equivalencia ↔ o10 o exclusivo ⊕


El siguiente cuadro es un resumen de los operadores booleanos más comunes:

x y ∧ ∨ → ↔ ⊕ ↑ ↓T T T T T T F F FT F F T F F T T FF T F T T F T T FF F F F T T F T T

Para notar la diferencia entre los operadores disyunción = "o inclusivo" y"o exclusivo". Interprete las frases :

“A las 8 en punto voy a ir al cine o voy a ir al teatro” = cine⊕teatro“La tierra gira alrededor del sol o 1 +1 = 2 ““La tierra gira alrededor del sol o 1 +1 = 3”

El operador p → q es llamado implicacion material, p es denominado elantecedente y q el concecuente.

La implicación material no contiene elementos de causalidad; esto lo puedenotar interpretando las siguientes frases:

“Si la tierra gira alrededor del sol entonces 1+1=3”“Si el sol gira alrededor de la tierra entonces 1+1=3”

Esta confusión puede ser solucionado haciendo referencia a la definición deeste operador en lugar de traducir al lenguaje natural.

Es facil mostrar que el conjunto operadodes {∧,∨,→,↔,¬} es redundante,pues con estos conjuntos operadores {∧,∨,¬} , {∧,¬} , {∨,¬} , {↑} y {↓} essuficiente para definir para definir todos los demas operadores.

La elección de un conjunto interesante de operadores depende de la aplica-cion. A las matemáticas le interesa la forma lógica de las deduciones. Dado unconjunto de axiomas , que implica?. Por lo que, la implicación y la negación sonlos operadores elegidos como base.

En el diseno digital de hardware digital, la lógica de “compuertas” se aplicancomunmente {∧,∨,¬} , {↑} y {↓}.

Los operadors binarios ↔ y ⊕ son sus propias inversas, esto es, ((p↔ q)↔q) ≡ p y ((p⊕q)⊕q) ≡ p . Esta propiedad es usada en circuitos y programas queimplementan la codificación para la corrección de errores y la criptografía. Unmensaje codificado es creado para la realización de una operación exclusiva entrelos datos y el código. Si CodedMessage ≡ Data⊕Code , entonces Data puederecuperarse mediante la realización de una operación CodedMessage⊕Code =(Data⊕ Code)⊕ Code = Data.


2.2.3. Definición:Una fórmula en lógica proposicional es es una oración que se puede obtener

de la siguiente gramática, a partir del símbolo no terminal fml.

1. fml ::= p , para todo p ∈ P

2. fml ::= ¬fml

3. fml ::= fml ∨ fml

4. fml ::= fml ∧ fml

5. fml ::= fml→ fml

6. fml ::= fml↔ fml

7. fml ::= fml ⊕ fml

8. fml ::= fml ↑ fml

9. fml ::= fml ↓ fml

El conjunto de fórmulas que pueden ser derivadas por esta gramatica es denotadocon F (G) .

2.2.4. Ejemplo:El árbol de derivación de la fórmula p → q ↔ ¬p → ¬q es dada en la si-

guiente figura:

fig1Del árbol de derivación obtenemos un árbol de formación de fórmulas, re-

emplazando el símbolo no terminal fml por su hijo que es un operador o unátomo, como se muestra en la siguiente figura:fig2

La formula “la oracion en el lenguaje generado por la gramatica” se puedeleer de izquierda a derecha recorriendo las hojas del arbol de derivacion o conun recorrido inorden del arbol de formacion.

Desafortunadamente, esta secuencia lineal de símbolos es también obtenidadel árbol de formación mostrada en la figura:

lo que representa una fórmula completamente diferente.En otras palabras, la representacion lineal de fórmulas es ambigua, aunque

los árboles de formación no lo son. Ya que se prefiere tratar con sequencias li-neales de símbolos, nececitamos resolver las ambiguedades si se quiere utilizaruna representacion lineal de una fórmula independientemente de su derivación.Hay tres maneras de hacer esto.


No habrá ambigüedad si la secuencia lineal de símbolos es creado por unrecorrido en preorden del árbol de formación. La representacion lineal de lasdos fórmulas son: ↔→ pq → ¬p¬q para el primer árbol y → p ↔ q¬ → p¬qpara el segundo árbol y ya no hay ambigüedad. Las fórmulas se dice que estánen notación polaca2 .

La notación polaca es difícil de leer para la mayoría de nosotros, porque laoperadores puede estar muy lejos de los operandos, por otro lado, la notacióninfija es más fácil de analizar mentalmente para nosotros . La notación polacase utiliza en la representación interna de una expresión en un ordenador y en elfuncionamiento de algunas calculadoras. La ventaja de la notación polaca es quela expresión puede ser ejecutado o calculado en el orden lineal de los símbolosque aparecen. Si queremos reescribir la primera fórmula q¬p¬ → qp →↔ ,puede ser compilado directamente por la siguiente secuencia de instrucciones deun resumen en lenguaje ensamblador:

1. Load q

2. Negate

3. Load p

4. Negate

5. Imply

6. Load q

7. Load p

8. Imply

9. Equiv

La segunda forma de resolver la ambigüedad es usar paréntesis. La gramáticasería cambiada a:

1. fml ::= p , para todo p ∈ P

2. fml ::= (¬fml )

3. fml ::= ( fml ∨ fml )

4. fml ::= ( fml ∧ fml )

5. fml ::= ( fml→ fml )

6. fml ::= ( fml↔ fml )

7. fml ::= ( fml ⊕ fml )

8. fml ::= ( fml ↑ fml )2Nombre del grupo de lógica dirigida por el polaco por J. Lukasiewicz.


9. fml ::= ( fml ↓ fml )

Las siguientes fórmulas están representados por diferentes cadenas y no hayambigüedad:

((p→ q)↔ ((¬q)→ (¬p)))

(p→ (q ↔ (¬(p→ (¬q)))))

El problema con los paréntesis es que las fórmulas se hacen difíciles de leer.

La tercera forma de la ambiguedad de fórmulas es definir precedencia y aso-ciatividad por convenios entre los operadores como se hace en aritmética, porlo que de inmediato reconocen a ∗ b ∗ c + d ∗ e = (((a ∗ b) ∗ c) + (d ∗ e)) . Enlógica proposicional el orden de precedencia de mayor a menor es el siguiente:negación, conjuncion , NAND, disyuncion, NOR, implicacion, eqivalence. Losoperadores se supone asociativos por la derecha, es decir: a∨b∨c = (a∨ (b∨c)).Los paréntesis se utilizan únicamente si es necesario para indicar un orden dife-rente del que impone la precedencia, al igual que en aritmética, donde a∗ (b+ c)necesita paréntesis para indicar que la adición se realiza antes de la multiplica-ción, mientras que a ∗ b+ c no lo necesita para denotar la multiplicación antesde sumar. Con un mínimo uso de paréntesis, las fórmulas de arriba se puedenescribir asi :

p→ q ↔ ¬q → ¬p

p→ (q ↔ ¬(p→ ¬q))

Cualquiera que sea la sintaxis que utilicemos para la representación lineal deuna fórmula, debe entenderse como una forma abreviada e inequivoca del árbolde formación.

2.2.5. Teorema:SiA ∈ F (G) emtonces A es una fórmula, entonces A es un átomo o tiene la

forma ¬A o A1op A2 para algunas fórmulas A1, A2y algún operador op.

2.2.6. Definición:Si A no es un átomo, el operador que se encuentra en la raíz del árbol de

formación, se denomina : el operador principal de la fórmula.Se utiliza Inducción Estructural para demostrar que si se verifica una pro-

piedad, esta se mantiene para todas las fórmulas: en primer lugar, se demostra:que vale para los átomos y, a continuación, se demostra que la propiedad seconserva cuando las fórmulas se construyen a partir de fórmulas más sencillasutilizando operadores.


2.2.7. Teorema: (Inducción Estructural)Para demostrar la propiedad(A) para todas las fórmulas A ∈ F (G) , es

suficiente demostrar que:

1. se verifica la propiedad(p) para todos los átomo p.

2. Si se verifica la propiedad(A)entonces propiedad(¬A) se verifica.

3. Si se verifica las propiedad(A1) y propiedad(A2) entonces propiedad(A1op A2)se verifica para cada operador op.

2.3. Lógica de Proposiciones: Semántica

2.3.1. Definición:Una asignación es la función v : P → {T, F}, es decir , v asigna uno de los

valores de verdad T o F a cada átomo.La asiganción v puede ser extendida a la función v : F (G) → {T, F}, quellamaremos una interpretación , que asigna valores de verdad a las fórmulasinductivanmente como lo vemos en la siguiente figura.

A v(A1) v(A2) v(A)¬A1

¬A1

TF

FT

A1 ∨A2

A1 ∨A2

Fotherwise

Fotherwise

FT

A1 ∧A2

A1 ∧A2

Totherwise

Totherwise

TF

A1 → A2

A1 → A2

Totherwise

Fotherwise

FT

A1 ↑ A2

A1 ↑ A2

Totherwise

Totherwise

FT

A1 ↓ A2

A1 ↓ A2

Fotherwise

Fotherwise

TF

A1 ↔ A2

A1 ↔ A2

v(A1) = v(A2)v(A1) 6= v(A2)

TF

A1 ⊕A2

A1 ⊕A2

v(A1) 6= v(A2)v(A1) = v(A2)

TF

2.3.2. Ejemplo:Sea A = (p→ q)↔ (¬q → ¬p) ,y sea v(p) = F , v(q) = T y v(pi) = T para

todos los otros pi ∈ P . Extendiendo v a una interpretación. El valor de verdadde A puede ser calculado en forma inductiva asi:

v(p→ q) = T


v(¬q) = F

v(¬p) = T

v(¬q → ¬p) = T

v((p→ q)↔ (¬q → ¬p)) = T

Puesto que cada fórmula A es representado por un único árbol de formación, vesta bien definida.

El uso de v para denotar tanto una asignación y una interpretación se justi-fica por el siguiente teorema.

2.3.3. Teorema:La función de asignación puede ser extendida a una función de interpretación.

Además, una interpretación no necesita hacer una asignación a todoslos posibles átomos de P .

2.3.4. Teorema:Sea P ′ = {pi1 , · · · , pin} ⊆ P los átomos que aparecen en A ∈ F (G) . Sean

v1y v2las asignaciones que estan de acuerdo con P ′ , tales que v1(pik) = v2(pik)para todo pik ∈ P ′ . Entonces la interpretación sobre A es tal que v1(A) = v2(A).

2.3.5. Definición:Sea S = {A1, · · · , An} un conjunto de fórmulas y sea v una asignación de

valores de verdad sobre todos los átomos que aparecen en cada Ai . Una inter-pretación, obtenida por la extención de v a todos las fórmulas en S es llamadauna interpretación para S .

2.3.6. Ejemplo:Sea A = {p→ q , p, p ∨ s↔ s ∧ q}, y sea v una asignación dada por: v(p) =

T , v(q) = F , v(r) = T , v(s) = T . Entonces,v es una interpretación para Spues se pueden asignar los valores de verdad :v(p→ q) = Fv(p) = Tv(p ∨ s↔ s ∧ q) = F

2.3.7. Definición:Sea A1, A2 ∈ F (G). Si v(A1) = v(A2) para toda interpretación v , entonces

A1 es logicamente equivalente a A2, lo que denotamos con A1 ≡ A2.Por supuesto, es suficiente comprobar la interpretación para los valores verdadde los átomos que aparecen en cualquiera de estas fórmulas.


2.3.8. Ejemplo:¿Es la fórmula p ∨ q lógicamente equivalente a q ∨ p ?

Hay cuatro diferentes asignaciones para los átomos p y q :

p q v(p ∨ q) v(q ∨ p)T T T TT F T TF T T TF F F F

Puesto que p ∨ q y q ∨ p son iguales en todas las interpretaciones : p ∨ q≡ q ∨ p .

Este resultado puede ser generalizado para la conmutatidad de la disyunciónde dos fórmulas, y no sólo para la conmutatividad de la disyunción de los átomosp y q.

2.3.9. Teorema:Sean A1 y A2 fórmulas en F (G) , entonces A1 ∨A2 ≡ A2 ∨A1.

PruebaSi v es una interpretación arbitraría para A1∨A2, es decir , v es una asignación devalores de verdad para la unión del conjunto de átomos de A1y A2 . Obviamente,v es tambien una interpretación para A2∨A1 . Además, puesto que el conjunto deátomos en A1 es un subconjunto de los átomos en A1∨A2, v es una interpretaciónpara A1 , analogamente para A2, de donde:v(A1∨A2) = T ⇐⇒ v(A1) = T ó v(A2) = T ⇐⇒ v(A2∨A1) = T por definición.Puesto que v es arbitraría A1 ∨A2 ≡ A2 ∨A1.

2.3.10. Observación:1. ≡ no es un operador booleano , es simplemente una notación para la frase

”es lógicamente equivalente a” , mientras que ↔ es un operador booleanoen lógica proposicional.

2. Existe la posibilidad de confusión en el estudio de la lógica porque estamosutilizando un vocabulario similar tanto para el lenguaje de objetos dedebate, en este caso la lógica proposicional, y para el lenguaje semiformalmetamatemático, que utiliza razonamientos sobre el lenguaje objeto.

3. Del mismo modo, hay que distinguir entre una fórmula proposicional p∨ qen el lenguaje objeto y una fórmula A1 ∨A2 en el metalenguaje.

2.3.11. Teorema:Si A1 ≡ A2 si y sólo si A1 ↔ A2 es verdadera para toda interpretación.


2.3.12. Definición:A es una subfórmula de B si el árbol de formación para A es producida como

un subárbol de formación del árbol de B. A es una subfórmula propia para Bsi A es una subfórmula de B , pero A no es identicamente a B .

2.3.13. Ejemplo:La fórmula (p→ q)↔ (¬p→ ¬q) contiene las siguientes subfórmulas : p→ q

, ¬p→ ¬q , ¬q , ¬p , q y p .

2.3.14. Definición:Sea A una subfórmula de B y sea A′ alguna fórmula , B′ = B {A← A′} es

la fórmula obtenida reemplazando todas las ocurrencias de los subárboles de Aen B por el árbol de A′.

2.3.15. Ejemplo:Sea B = (p→ q)↔ (¬p→ ¬q) , A = p→ q y A′ = ¬p ∨ q

B′ = B {A← A′}

= B {A← ¬p ∨ q}

= (¬p ∨ q)↔ (¬p→ ¬q)

2.3.16. Teorema:Si A una subfórmula de B y sea A′ la fórmula tal que A ≡ A′ , entonces

B ≡ B {A← A′} .

2.3.17. Fórmulas Lógicamente EquivalentesA ∨ true ≡ true A ∧ true ≡ A

A ∨ false ≡ A A ∧ false ≡ false

A→ true ≡ true true→ A ≡ A

A→ false ≡ ¬A false→ A ≡ true

A↔ true ≡ A A⊕ true ≡ ¬A

A↔ false ≡ ¬A A⊕ false ≡ A


A ≡ ¬¬A

A ≡ A ∧A A ≡ A ∨A

A ≡ A→ A ≡ true

A ∨ ¬A ≡ true A ∧ ¬A ≡ false

A↔ A ≡ true A⊕A ≡ false

¬A ≡ A ↑ A ¬A ≡ A ↓ A

A ∨B ≡ B ∨A A ∧B ≡ B ∧A

A↔ B ≡ B ↔ A A⊕B ≡ B ⊕A

A ↑ B ≡ B ↑ A A ↓ B ≡ B ↓ A

A→ B ≡ ¬B → ¬A

A ∨ (B ∨ C) ≡ (A ∨B) ∨ C A ∧ (B ∧ C) ≡ (A ∧B) ∧ C

A↔ (B ↔ C) ≡ (A↔ B)↔ C A⊕ (B ⊕ C) ≡ (A⊕B)⊕ C

A ↑ (B ↑ C) ≡ (A ↑ B) ↑ C A ↓ (B ↓ C) ≡ (A ↓ B) ↓ C

A ∨ (B ∧C) ≡ (A ∨B) ∧ (A ∨C A ∧ (B ∨C) ≡ (A ∧B) ∨ (A ∧C)

A ∧ (A ∨B) ≡ A A ∨ (A ∧B) ≡ A

A↔ B ≡ (A→ B) ∧ (B → A) A⊕B ≡ ¬(A→ B) ∨ ¬(B → A)

A→ B ≡ ¬A ∨B A→ B ≡ ¬(A ∧ ¬B)

A ∨B ≡ ¬(¬A ∧ ¬B) A ∧B ≡ ¬(¬A ∨ ¬B)

A ∨B ≡ ¬A→ B A ∧B ≡ ¬(A→ ¬B)

A→ B ≡ A↔ (A ∧B) A→ B ≡ B ↔ (A ∨B)

A ∧B ≡ (A↔ B)↔ (A ∨B) A↔ B ≡ (A ∨B)→ (A ∧B)


2.3.18. Observaciones:1. Ampliamos la grámatica booleana de fórmulas para incluir las proposicio-

nes atómicas constantes true y false. Haciendo : fml ::= true/false

2. Interprete como v(true) = T y v(false) = F para cualquier v. Es posibleconsiderar true y false como abreviaciones de las fórmulas p∨¬p y p∧¬prespectivamente.

3. No confundir estos símbolos en el lenguaje objeto la lógica proposicionalcon los valores de verdad T y F usadas para definir las interpretaciones.

4. La simplificación es una de las más importantes aplicaciones de la susti-tución de equivalencias lógicas . Por ejemplo :

2.3.19. Definición:Un operador binario o es definido desde el conjunto de los operadores {o1, · · · , on}

si y sólo si existe una equivalencia lógicaA1oA2 ≡ A dondeA es una fórmula con-truida a partir de las ocurrecias de A1 y A2 usando los operadores {o1, · · · , on} .Similarmente, el operador unario ¬ es definida por la fórmula ¬A1 ≡ A , dondeA es construida a partir de las ocurrencias de A1 y el conjunto de operadores.

2.3.20. Ejemplo:

A↔ B ≡ (A→ B) ∧ (B → A)

A→ B ≡ ¬A ∨B A→ B ≡ ¬(A ∧ ¬B)

A ∨B ≡ ¬(¬A ∧ ¬B) A ∧B ≡ ¬(¬A ∨ ¬B)

¬A ≡ A ↑ A

A ∧ B ≡ (A ↑ B) ↑ (A ↑ B) De las fórmulas de negación y conjunción, todoslos demás operadores puede ser definidos. Del mismo modo las definiciones sonposibles sólo NAND .

2.3.21. Teorema:Si o un operador binario tal que puede definirse la negación y todos los otros

operadores , entonces o es uno de ellos : nand ó nor .


2.4. Satisfacibilidad , Validez y Consecuen-cia

2.4.1. Definición:Una fórmula proposicional A es satisfacible si sólo si v(A) = T para alguna

interpretación v . Una interpretación satisfacible, es llamada un modelo paraA . Una fórmula A es válida , que denotamos con |= A si y sólo si v(A) = Tpara todas las interpretaciones v . Una fórmula proposicional válida es llamadatautología .Una fórmula proposicional A no satisfacible o contradictoria si y sólo si v(A) = Fpara todas las interpretaciones de v .Una fórmula A es no válida que denotamos con 2 A si sólo si v(A) = F paraalguna interpretación v .

2.4.2. Teorema:A es válida si y sólo si ¬A es contradictoria . A es satisfacible si y sólo si ¬A

no es válida.

2.4.3. Definición:Sea Ψ un conjunto de fórmulas . Un algoritmo es un procedimiento de de-

cisión para Ψ, si dada una fórmula arbitraría A ∈ F (G) , este procedimientotermina y retorna la respuesta “yes” si A ∈ Ψ y “no” A /∈ Ψ .

2.4.4. Observación:Por el Teorema 2.4.2, un procedimiento de decisión para la satisfacibilidad

puede ser usado como un procedimiento de decisión la validez. Para decidir siA es válida , aplicar el algoritmo para la satisfasibilidad de ¬A . Si reporta que¬A es satisfasible , entonces A es no válida ; si el algoritmo reporta que ¬A escontradictoria , entonces A es válida. Tal algoritmo es llamado un procedimientode refutación , pues provamos la valides de una fórmula refutando su negación,tal procedimiento de decisión se llama una refutación . Refutación suele ser unprocedimiento más eficiente, porque en lugar de comprobar que la fórmula essiempre verdadera , sólo tenemos que buscar un contraejemplo para su negación.

La existencia de un procedimiento para la satisfasibilidad en lógica proposi-cional es trivial. Puesto que una fórmula contiene un número finito de átomos,entonces existe un número finito de interpretaciones diferentes y podemos com-probar todos ellos. Este algoritmo es llamado el método de las tablas de verdadpuesto que la computación puede ser organizada en forma tabular.


2.4.5. Ejemplo:La fórmula (p→ q)→ (¬q → ¬p) es válida porque cada linea de la tabla de

verdad es T.

p q p→ q ¬q → ¬p (p→ q)→ (¬q → ¬p)T T T T TT F F F TF T T T TF F T T T

2.4.6. Ejemplo:La fórmula p ∧ q es satisfasible pero no es válida

p q p ∧ qT T TT F FF T FF F F

2.4.7. Ejemplo:La fórmula (p ∨ q) ∧ ¬p ∧ ¬q es contradictoría

p q p ∨ q ¬p ¬q (p ∨ q) ∧ ¬p ∧ ¬qT T T F F FT F T F T FF T T T F FF F F T T F

El método de las tablas de verdad es un algoritmo muy ineficiente por queevalua la fórmula para cada una de las 2n posibles interpretaciones, donde nes el número de los diferentes átomos en la fórmula . En las siguiente seccionesdiscutiremos algoritmos más eficientes.

2.4.8. Definición:Un conjunto de fórmulas U = {A1, · · · , An}es (simultaneamente) satisfasible

si y sólo si existe una interpretación v tal que v(A1) = · · · = v(An) = T , dichainterpretación es llamado un modelo para U . U es contradictoría si y sólo sipara cada interpretación v existe una i tal que v(Ai) = F .

2.4.9. Ejemplo:El conjunto U1 = {p , ¬p ∨ q , q ∧ r } es simultaneamente satisfacible por

la interpretación que asigna T a cada átomo , mientras que el conjunto U2 =


{p , ¬p ∨ q , ¬p }es contradictorio . Observe que cada fórmula en U2es satisfacible, pero no son satisfacibles simultaneamente.

2.4.10. Teorema:Si U = {A1, · · · , An}es satisfacible , entonces también lo es U − {Ai} para

algún 1 ≤ i ≤ n .

2.4.11. Teorema:Si U = {A1, · · · , An} es contradictoria y para algún 1 ≤ i ≤ n, Ai es válida

, entonces U − {Ai} es contradictoria.

2.4.12. Definición:Sea U un conjunto de fórmulas y A una fórmula . Si A es verdadera en todo

modelo de U , entonces A es una consecuencia lógica de U . Lo que se denotacon : U |= A.

A no tiene por qué ser verdadera en todas las posibles interpretaciones,sólo en esas interpretaciones que son modelo en U . Si U está vacío, laconsecuencia lógica es la misma válidez de A.

2.4.13. Ejemplo:Sea A = (p∨r)∧(¬q∨¬r) . Entonces A es una consecuencia lógica de {p,¬q},

entonces {p,¬q} |= A , puesto que A es verdadera en todas las interpretacionestales que v(p) = T y v(q) = F . Sin embargo, A no es válida , puesto que no esverdadera en toda interpretación: v(p) = F , v(q) = T , v(r) = T .

La advertencia concerniente a ↔ y ≡ también se aplica a → y |= . → esun operador en el lenguaje objeto y |= es un símbolo de un concepto en elmetalenguaje.

2.4.14. Teorema:Sea U = {A1, · · · , An}. U |= A si y sólo si |= A1∧, · · · ∧An → A

2.4.15. Teorema:Si U |= A y B es válida entonces U − {B} |= A .

2.4.16. Observación:La consecuencia lógica es un concepto central en el fundamento de las ma-

temáticas. Fórmulas válidas tales como p ∨ q ↔ q ∨ p son de poco interés paralas matemáticas puesto que son evidentes . Es mucho más interesante asumir


que un conjunto de fórmulas son verdaderas y, a continuación investigar lasconsecuencias de estos supuestos.

2.5. Tableau Semántico

El método Tableau Semántico es un algoritmo relativamente eficiente paradecidir satisfasibilidad (y la dualidad de la validez) en lógica proposicional .Más aún , el método es importante por que será la principal herramienta parademostrar teoremas generales sobre lógica. El principio es muy simple: la bús-queda sistemática de un modelo. Si uno lo encuentra, la fórmula es válida, delo contrario, es contradictoría. Empezamos con la definición de algunos térmi-nos y, a continuación, analizamos la validez de dos fórmulas para motivar laconstrucción del Tableau Semántico .

2.5.1. Definición:Una literal es un átomo o la negación de un átomo. Un átomo es una literal

positiva y la negación de un átomo es una literal negativa. Para algún átomop , {p,¬p} es un par complementarío de literales. Para alguna fórmula A ,{A,¬A}es un par complementarío de fórmulas. A es el complemento de ¬A y¬A es el complemento de A .

2.5.2. Ejemplo:Vamos a analizar la validez de la fórmula A = p ∧ (¬q ∨ ¬p) en una inter-

pretación arbitraria v. Utilizaremos el método inductivo , para la evaluación delvalor de verdad de una fórmula.

v(A) = T sii v(p) = T y v(¬q ∨ ¬p) = T

Por lo tanto , v(A) = T sii se cumple :

1. v(p) = T y v(¬q) = T ó

2. v(p) = T y v(¬p) = T

Por lo tanto, A es válido si y sólo si hay una interpretación tal que (1) ó (2) semantienen.

Hemos reducido la cuestión de la validez de la A a la pregunta sobre la sa-tisfacibilidad de conjuntos de literales. Es fácil ver que un conjunto de literaleses válido si y sólo si no contiene un pares de literales complementarias. Ya quecualquier fórmula contiene un número finito de átomos, hay a lo sumo un nú-mero finito de conjuntos de literales, construida a partir de estos átomos. Esfacil decidir si la condición se mantiene para algún conjunto de literales. En elejemplo, el segundo conjunto de literales {p,¬p} es complementaria y, por tanto,contradictoría , pero el primer conjunto {p,¬q}no contiene ningún par de litera-les complementarias , por lo tanto, el conjunto es satisfacible y podemos concluir


que A es también satisfacible. Por otra parte, podemos construir un modelo deA con asignación de T para literales positivos y F literales negativos:v(p) = T, v(q) = F .

!comprobar que para esta interpretación v(A) = T !.

2.5.3. Ejemplo:Consideremos la fórmula B = (p ∨ q) ∧ (¬p ∧ ¬q) .

v(B) = T sii v(p ∨ q) = T y v(¬p ∧ ¬q) = T .

Por lo tanto, v(B) = T sii v(p ∨ q) = v(¬p) = v(¬q) = T .

Por lo tanto, v(B) = T sii se cumple :

1. v(p) = v(¬p) = v(¬q) = T , ó

2. v(q) = v(¬p) = v(¬q) = T .

Ya que ambos conjuntos de literales {p,¬p,¬q} y {q,¬p,¬q} contienen parescomplementarios, el conjunto de literales no es válido y conluimos que es impo-sible encontrar un modelo para B, es decir, B es contradictorio.

Búsqueda sistemática, es llevar a cabo un seguimiento de las tareas que debenrealizarse en la estructura de datos utilizada para construir las subfórmulas. Enel Tableau Semántico , los árboles utilizan : la raíz como etiqueta de la fórmulaoriginal, y los conjuntos de fórmulas creadas por la de búsqueda interior etique-tan los nodos del árbol. Las hojas serán etiquetadas de conjuntos de literalesque deben satisfacerse. Una hoja que contiene un conjunto complementario deliterales se marcarán x, mientras que una hoja que es satisfacible será marcadacon �. A continuación presentamos el Tableau Semántico para las fórmulas Ay B de los ejemplos

p ∧ (¬q ∨ ¬p) (p ∨ q) ∧ (¬p ∧ ¬q)↓ ↓

p, ¬q ∨ ¬p p ∨ q,¬p ∧ ¬q↙ ↘ ↓

p,¬q p,¬p p ∨ q,¬p,¬q� x ↙ ↘

p,¬p,¬q q,¬p,¬qx x

La construcción del Tableau semántico no es única, aquí otro tableau para(p ∨ q) ∧ (¬p ∧ ¬q).

Es construido por busqueda de ramificación para satisfacer (p ∨ q) antes debuscar satisfacer ¬p∧¬q .Claramente, el primer cuadro es más eficiente debidoa que contiene un menor número de nodos


(p ∨ q) ∧ (¬p ∧ ¬q)↓

p ∨ q,¬p ∧ ¬q↙ ↘

p,¬p ∧ ¬q q,¬p ∧ ¬q↓ ↓

p,¬p,¬q q,¬p,¬qx x

Una descripción concisa de las reglas para la creación de un Tableau Se-mántico se puede dar si las fórmulas se clasifican según su principal operador.Si la fórmula es una negación, la clasificación tiene en cuenta la negación y eloperador principal . Hay dos tipos de reglas: las α− formulas conjuntivas queson satisfacibles si y sólo si ambas subfórmulas α1 y α2 son satisfacibles , y lasβ−formulas disyuntivas que son satisfacibles si y sólo si una de las subfórmulasβ1 ó β2 es satisfacible.

Lo que determina, la siguiente tabla de clasificación , para la cons-trucción de un Tableau semántico

α α1 α2

¬¬A1 A1

A1 ∧A2 A1 A2

¬(A1 ∨A2) ¬A1 ¬A2

¬(A1 → A2) A1 ¬A2

¬(A1 ↑ A2) A1 A2

A1 ↓ A2 ¬A1 ¬A2

A1 ↔ A2 A1 → A2 A2 → A1

¬(A1 ⊕A2) A1 → A2 A2 → A1

β β1 β2

¬(B1 ∧B2) ¬B1 ¬B2

B1 ∨B2 B1 B2

B1 → B2 ¬B1 B2

B1 ↑ B2 ¬B1 ¬B2

¬(B1 ↓ B2) B1 B2

¬(B1 ↔ B2) ¬(B1 → B2) ¬(B2 → B1)B1 ⊕B2 ¬(B1 → B2) ¬(B2 → B1)

2.5.4. Definición:Un Tableau , cuya construcción ha terminado , se llama un Tableau completo

. Un Tableau completo es cerrado si todas las hojas son marcadas como cerradas(x). En cualquier otro caso , el Tableau completo es llamado abierto , esto es ,si alguna hoja es marcada como abierta (�) .


2.5.5. Teorema :La construcción del Tableau semántico siempre termina.

2.5.6. Observación :En la práctica, la construcción de un Tableau semántico , puede ser más

eficiente :

1. Definir una hoja como no atómicamente cerrada si contiene un par defórmulas complementarias y definir como atómicamente cerrada si contieneun par de literales complementarias. Cambia el algoritmo para marcar unahoja cerrada si no es atómicamente cerrada. Se puede demostrar que elmétodo del Tableau semántico sigue siendo sólida y completa el marco deesta definición (más eficiente).

2. No es necesario copiar sin modificar las fórmulas de un nodo a otro. Im-portantes ahorros de tiempo y memoria se pueden lograr si la etiqueta deun nodo es un conjunto de punteros a las fórmulas propias.

3. Varias heurísticas pueden ser utilizadas para acortar el Tableau . Por ejem-plo, siempre utiliza α−reglas antes β−reglas a fin de evitar la duplicaciónde fórmulas.

2.5.7. Ejemplohfsdkjaskj

2.5.8. Teorema :Sea τ un Tableau completo para la fórmula A . A es contradictoria sii τ es

cerrada .

2.5.9. Corolario:A es satisfacible sii τ es abierta.

2.5.10. Corolario :A es válida si sólo si el Tableau para ¬A es cerrada .

2.5.11. Ejemplo :Ahora si A = p ∨ (q ∧ ¬q) su tableau es :


p ∨ (q ∧ ¬q)↙ ↘

p q ∧ ¬q� ↓

q , ¬qx

Desde la rama del tableau, podemos concluir que para cualquier modelo, sedebe definir que v(p) = T . Sin embargo, para una interpretación de A tambiénse debe definir una asignación para q . Es evidente en este caso que cualquierinterpretación que asigne T a p , es un modelo para A, independientemente delo que se ha asignado a la q .

2.6. Lógica Proposicional : Sistemas Deduc-tivos

2.6.1. Definición :Un sistema deductivo es un conjunto de axiomas y un conjunto de reglas de

inferencia . Una prueba en un sistema deductivo es una secuencia de conjuntosde fórmulas tales que cada elemento es o bien un axioma o se puede deducirde los anteriores elementos de la secuencia utilizando una regla de inferencia.Si A es el último elemento de la secuencia, A es un teorema, la secuencia de laprueba de A, y que A es demostrable, se denota con ` A .

2.6.2. Observación :1. El concepto de deducir el teorema de un conjunto de axiomas y reglas es

muy antigua y está familiarizado con cada estudiante de secundaria porla geometría Euclideana . La Matemática moderna, con sus millones deteoremas, se expresa en un estilo de razonamientos y no esta muy lejosde el razonamiento usado por los matemáticos griegos. Este estilo puedecaracterizarse como “formalizado razonamiento informal” , en el sentidode que, si bien las pruebas se expresan en lenguaje natural en lugar de enun sistema formal, hay convenios entre los matemáticos , como las formasde razonamiento que se les permite . El sistema deductivo que estudiare-mos son las formalizaciones del razonamiento usado en matemáticas, y sedesarrollaron en un intento de justificar el razonamiento matemático .

2. Deducción es puramente sintáctico:

Puede haber un número infinito de axiomas, pero sólo aparecerá unnúmero finito en alguna prueba .

Cualquier prueba en particular, consiste en una secuencia finita deconjuntos de fórmulas, y la habilidad de cada persona para deducirlacon facilidad y eficacia a partir de la sintaxis de las fórmulas .


La prueba de una fórmula claramente se demuestra con axiomas,teoremas y reglas que son usadas . Este patrón puede ser transfe-rido a otras pruebas similares, o modificados para probar diferentesresultados .

Una vez que un teorema ha quedado demostrado, puede ser utilizadoen las pruebas como un axioma .

Deducción introduce nuevos problemas. Aunque se define en términos puramen-te sintácticos de la fórmula de manipulación, no es susceptible de un procedi-miento sistemático de búsqueda . El tableau semántico sólo crea subformulas dela fórmula que deben probarse (o sus negaciones). En la mayoría de los sistemasdeductivo, cualquier axioma puede ser utilizado, independientemente de si setrata de una subformula de la fórmula que deben probarse. La deducción esmás difícil porque requiere ingenio en lugar de buscar a fuerza bruta, aunquelos programas, llamados prueba automática de teoremas, usan heurísticas paraorientar la búsqueda de una prueba.

2.6.3. El Sistema de Gentzen G

2.6.3.1. Definición :

El Sistema de Gentzen G es un sistema deductivo . Los axiomas son losconjuntos de fórmulas que contienen un par complementario de literales . Lasreglas de inferencia son :

Ù1∪{α1,α2}Ù1∪{α}

Ù1∪{β1} Ù2∪{β2}Ù1∪U2∪{β}

El conjunto o conjuntos de fórmulas por encima de la línea se llaman premisasy el conjunto de fórmulas debajo de la línea se llama conclusión .Donde la clasificación en α−formula y β−formula es el dual de la clasificaciónpara el Tableau Semántico .

α α1 α2

A ¬¬A¬(A1 ∧A2) ¬A1 ¬A2

A1 ∨A2 A1 A2

A1 → A2 ¬A1 A2

A1 ↑ A2 ¬A1 ¬A2

¬(A1 ↓ A2) A1 A2

¬(A1 ↔ A2) ¬(A1 → A2) ¬(A2 → A1)A1 ⊕A2 ¬(A1 → A2) ¬(A2 → A1)


β β1 β2

B1 ∧B2 B1 B2

¬(B1 ∨B2) ¬B1 ¬B2

¬(B1 → B2) B1 ¬B2

¬(B1 ↑ B2) B1 B2

B1 ↓ B2 ¬B1 ¬B2

B1 ↔ B2 B1 → B2 B2 → B1

¬(B1 ⊕B2) B1 → B2 B2 → B1

2.6.4. Observacion :1. El conjunto de fórmulas enG es una disyunción implicita , como un axioma

que contienen un par complementario de literales que obviamente es válido. Para una α−formula , la inferencia de U1∪{A1, A2} a U1∪{A1 ∨A2}(ocualquier otro de los operadores disyuntivos) es simplemente una forma-lización del significado de un conjunto como una disyunción . Para unaβ − formula , si hemos demostrado tanto tU1 ∨B1 y tU2 ∨B2 entoncestU1 ∨tU2 ∨ (B1 ∧B2) se infiere mediante la distribución de la disyunciónsobre la conjunción . ( La notación tU significa la disyunción sobre todaslas fórmulas en U).

2. La prueba está escrita como una secuencia de conjuntos de fórmulas queestán numeradas para referencia conveniente . A la derecha de cada líneaesta su justificación: o bien el conjunto de fórmulas es un axioma, o es laconclusión de una regla de inferencia aplicada a un conjunto o conjuntos defórmulas anteriores en la secuencia. Una regla de inferencia es identificadocomo α − regla ó β − regla en el operador principal de la conclusión yel número o los números de las líneas que contienen las premisas . Enel sistema G podemos escribir ` {A1, A2, · · · , An}o sin los parentesis `A1, A2, · · · , An .

2.6.5. Ejemplo :` (p ∨ q)→ (q ∨ p) . La prueba es :

1. ` ¬p, q, p Axioma

2. ` ¬q, q, p Axioma

3. ` ¬(p ∨ q), q, p β∨, 1, 2

4. ` ¬(p ∨ q), (q ∨ p) α∨, 3

5. ` (p ∨ q)→ (q ∨ p) α→, 4


2.6.6. Ejemplo :` (p ∨ (q ∧ r))→ (p ∨ q) ∧ (p ∨ r) . La prueba es :

1. ` ¬p, p, q Axioma

2. ` ¬p, (p ∨ q) α∨, 1

3. ` ¬p, p, r Axioma

4. ` ¬p, (p ∨ r) α∨, 3

5. ` ¬p, (p ∨ q) ∧ (p ∨ r) β∧, 2, 4

6. ` ¬q,¬r, p, q Axioma

7. ` ¬q,¬r, (p ∨ q) α∨, 6

8. ` ¬q,¬r, p, r Axioma

9. ` ¬q,¬r, (p ∨ r) α∨, 8

10. ` ¬q,¬r, (p ∨ q) ∧ (p ∨ r) β∧, 7, 9

11. ` ¬(q ∧ r), (p ∨ q) ∧ (p ∨ r) α∧, 10

12. ` ¬(p ∨ (q ∧ r), (p ∨ q) ∧ (p ∨ r) β∨, 5, 11

13. ` (p ∨ (q ∧ r)→ (p ∨ q) ∧ (p ∨ r) α→, 12

Observe que hemos sido bastante inteligentes para organizar todas las inferenciasen las pruebas para que todo salga exactamente al final. Vamos a reorganizar laprueba de Gentzen en un formato de árbol en lugar de una secuencia lineal deconjuntos de fórmulas. Que los axiomas sean las hojas del árbol, y dejar que lasreglas de inferencia definan los nodos en el interior. La raíz en la parte inferiorse etiqueta con la fórmula que se demuestre.

2.6.7. Ejemplo :La prueba de los ejemplos se muestra en forma de árbol :

¬p, q, p ¬q, q, p ¬ ((p ∨ q)→ (q ∨ p))↘ ↙ ↓¬ (p ∨ q) , q, p p ∨ q,¬ (q ∨ p)

↓ ↓¬ (p ∨ q) , (q ∨ p) p ∨ q,¬q,¬p

↓ ↙ ↘(p ∨ q)→ (q ∨ p) p,¬q,¬p q,¬q,¬p

x xLo que hemos hecho es escribir el Tableau semántico al revés e invertir los

signos de las fórmulas que aparecen en las etiquetas de los nodos, tal y como semuestra a la derecha de la figura de derivación Gentzen .


Si la etiqueta de una hoja en un Tableau semántico contiene α − formulase amplía con un nodo cuya etiqueta contiene {α1, α2}, luego desde ` {α1, α2}podemos deducir en ` α en G . (recordar que las fórmulas en G son duales a lasdel Tableau semántico ). Del mismo modo, si la etiqueta de una hoja contieneuna β − formula se amplía con nodos cuyas etiquetas contienen β1 y β2 de la` β1 y ` β2, luego podemos deducir ` β en G . El lector debe verificar estasafirmaciones comparando la prueba con el árbol semántico cuadro en el ejemplo2.25 .

La relación semántica entre el Tableau y los sistemas de Gentzen se formalizaen el siguiente teorema.

2.6.8. Teorema :Sea U un conjunto de fórmulas y U el conjunto de fórmulas complementarias

en U . Entonces ` U en G si sólo si existe un Tableau semántico cerrado paraU .

2.6.9. Corolario :` A en G si sólo si exixte un Tableau semántico cerrado para ¬A .

2.6.10. Teorema : ( Solidez y Compleción de G )|= A si sólo si ` A en G .

El sistema de Gentzen G descrito en esta sección no es muy útil ; otrasversiones que veremos adelante son más convenientes para provarteoremas y están más cerca de la formulación original de Gentzen. Hemos introducido G como un escalón teórico a los sistemas deHilbert que ahora describiremos .

2.7. El Sistema de Hilbert H

En los sistemas Gentzen existe muchos axiomas y dos reglas, mientras queen un sistema de Hilbert hay 3 axiomas y sólo una regla . Este libro de texto(como la mayoría de los otros) sólo contiene un teorema (Teorema 2.7.2), quese prueba directamente, el uso práctico del sistema depende de la utilización delas reglas de derivación, especialmente la regla de deducción .

2.7.1. Definición :H es un sistema deductivo con tres esquemas de axiomas y un regla de

inferencia . Para cualesquiera fórmulas A,B,C , las siguientes fórmulas sonaxiomas :

Axioma 1 ` (A→ (B → A)) .


Axioma 2 ` ((A→ (B → C))→ ((A→ B)→ (A→ C)) .

Axioma 3 ` (¬B → ¬A)→ (A→ B) .

La regla de inferencia es llamada Modus Ponens (MP) . Para cuales-quiera fórmulas A,B :

`A `A→B`B

Cuando un axioma es dado como la justificación, asegúrese de que puedeidentificar fórmulas que se sustituirán por la fórmula en el esquema del axioma.

2.7.2. Teorema :` A→ A .

Prueba

1. ` (A→ ((A→ A)→ A))→ ((A→ (A→ A))→ (A→ A)) Axioma 2

2. ` (A→ ((A→ A)→ A)) Axioma 1

3. ` (A→ (A→ A))→ (A→ A) MP 1,2

4. ` (A→ (A→ A)) Axioma 1

5. ` (A→ A) MP 3,4

La prueba es bastante complicada para una fórmula trivial. Con el fin de forma-lizar los poderosos métodos de inferencia utilizados en matemáticas, introduci-remos nuevas reglas de inferencia denominada reglas derivadas. Para cada regladerivada, demostraremos que la regla es solida : el uso de la regla de derivaciónno aumenta el conjunto de teoremas en H . Mostraremos como mecanicamentetransformar una prueba usando la regla de derivación dentro de otra ( usual-mente más larga) usando sólo los axiomas originales y MP . Por su puesto unavez que una regla de derivación ha sido probada su solidez esta puede ser usadaen la justificación de otra regla de derivación .

Las reglas de derivacion mas importantes son las reglas de deduccion: asumir la premisa de la implicacion que tu quieres probar y entoncesprobar la concecuencia .

2.7.3. Ejemplo :Supongamos que queremos demostrar que la suma de dos números impares

es par , expresado formalmente como : odd(x)∧odd(y)→ even(x+y) para todox , y . Supongamos la fórmula odd(x)∧odd(y) como un axioma adicional . Ahoraque tenemos a nuestra suposición y todos los teoremas que ya hemos deducido


acerca de los números, en particular, el teorema que cualquier número imparpuede expresado como : 2k+1 . Entonces x+y = 2k1+1+2k2+1 = 2(k1+k2+1)es un número par . La implicación odd(x)∧ odd(y)→ even(x+ y) se desprendede la regla de la deducción con los supuestos de asumidos.

2.7.4. Definición :Sea U un conjunto de fórmulas y A una fórmula . La notación U ` A significa

que las fórmulas en U son hipótesis en la prueba de A . Si Ai ∈ U , la pruebade U ` A puede incluir un elemento de la forma U ` Ai .

2.7.5. Regla de la Deducción :U∪{A}`BUÀ→B

2.7.6. Teorema de la deducción :La regla de la deducción es una regla derivada sólida .

2.7.7. Observación:Ahora demostraremos una serie de importantes teoremas que usaremos como

justificaciones para las reglas derivadas . Un teorema de la forma U ` A → Bjustifica la regla de derivación de la forma : UÀ

U`B simplemente aplicando MPsobre A y A→ B .

La regla contrapositiva es justificada por el Axioma 3 .

2.7.8. Regla Contrapositiva :U`¬B→¬AUÀ→B .

2.7.9. Teorema :` (A→ B)→ [(B → C)→ (A→ C)] .

Prueba

1. {A→ B,B → A,A} ` A Hipótesis

2. {A→ B,B → C,A} ` A→ B Hipótesis

3. {A→ B,B → C,A} ` B MP 1, 2

4. {A→ B,B → C,A} ` B → C Hipótesis

5. {A→ B,B → AC,A} ` C MP 3, 4


6. {A→ B,B → C} ` A→ C Deducción 5

7. {A→ B} ` [(B → C)→ (A→ C)] Dedución 6

8. ` (A→ B)→ [(B → C)→ (A→ C)] Dedución 7

2.7.10. Regla de la Transitividad :UÀ→B U`B→C

UÀ→C . Esta regla justifica el ”paso a paso” del desarrollode un teorema matemático ` A→ C a través de una serie de lemas . El antece-dente A del teorema es usado para probar el lema ` A→ B1 , cuyo consecuetees utilizado para demostrar el próximo lema ` B1 → B2 y así sucesivamentehasta el consecuente del teorema aparece como ` Bn → C . El uso reiterado dela regla de transitividad nos permite deducir ` A→ C .

2.7.11. Teorema :` [A→ (B → C)]→ [B → (A→ C)] .

Prueba

1. {A→ (B → C), B,A} ` A Hipótesis

2. {A→ (B → C), B,A} ` A→ (B → C) Hipótesis

3. {A→ (B → C), B,A} ` B → C MP 1, 2

4. {A→ (B → C), B,A} ` B Hipótesis

5. {A→ B,B → AC,A} ` C MP 3, 4

6. {A→ (B → C), B,A} ` A→ C Deducción 5

7. {A→ (B → C)} ` [B → (A→ C)] Dedución 6

8. ` [A→ (B → C)]→ [B → (A→ C)] Dedución 7

2.7.12. Regla de Intercambio de Antecedentes :UÀ→(B→C)U`B→(A→C) .

2.7.13. Teorema :` ¬A→ (A→ B) .


Prueba

1. {¬A} ` ¬A→ (¬B → ¬A) Axioma 1

2. {¬A} ` ¬A Hipótesis

3. {¬A} ` ¬B → ¬A MP 1, 2

4. {¬A} ` (¬B → ¬A)→ (A→ B) Axioma 3

5. {¬A} ` A→ B MP 3, 4

6. ` ¬A→ (A→ B) Deducción 5

Si usted puede probar alguna fórmula y su negación, entonces no pue-de probar nada!! . Estudiaremos las consecuencias de este resultadomás adelante .

2.7.14. Teorema :` A→ (¬A→ B) .

Prueba

1. ` ¬A→ (A→ B) Teorema 2.46

2. ` A→ (¬A→ B) Intercambio 1

2.7.15. Teorema :` ¬¬A→ A .

Prueba

1. {¬¬A} ` ¬¬A→ (¬¬¬¬A→ ¬¬A) Axioma 1

2. {¬¬A} ` ¬¬A Hipótesis

3. {¬¬A} ` ¬¬¬¬A→ ¬¬A MP 1, 2

4. {¬¬A} ` ¬A→ ¬¬¬A Contrapositiva 3

5. {¬¬A} ` ¬¬A→ A Contrapositiva 4

6. {¬¬A} ` A MP 2, 5

7. ` ¬¬A→ A Deducción 6

2.7.16. Regla de la Doble Negación :U`¬¬AU`A .


2.7.17. Teorema :` (A→ B)→ (¬B → ¬A) .

Prueba

1. {A→ B,¬B,¬¬A} ` ¬¬A Hipótesis

2. {A→ B,¬B,¬¬A} ` A Doble Negación 1

3. {A→ B,¬B,¬¬A} ` A→ B Hipótesis

4. {A→ B,¬B,¬¬A} ` B MP 2, 3

5. {A→ B,¬B,¬¬A} ` ¬B Hipótesis

6. {A→ B,¬B,¬¬A} ` ¬B → (B → ¬¬B) Teorema 2.4.6

7. {A→ B,¬B,¬¬A} ` B → ¬¬B MP 5, 6

8. {A→ B,¬B,¬¬A} ` ¬¬B MP 4, 7

9. {A→ B,¬B} ` ¬¬A→ ¬¬B Deducción 8

10. {A→ B,¬B} ` ¬B → ¬A Contrapositiva 9

11. {A→ B,¬B} ` ¬B Hipótesis

12. {A→ B,¬B} ` ¬A MP 10, 11

13. {A→ B} ` ¬B → ¬A Deducción 12

14. ` (A→ B)→ (¬B → ¬A) Deducción 13

La regla contrapositiva puede ser formulada en la dirección opuesta .Similarmente , el otro sentido de la regla de doble negación se justificapor el siguiente teorema .

2.7.18. Teorema :` A→ ¬¬A .

Prueba

1. ` ¬¬¬A→ ¬A Teorema 2.4.8

2. ` A→ ¬¬A Contrapositiva 1

Si true es una abreviación de p → p y false es una abreviación de¬ (p→ p). Tenemos por ` true por el teorema 2.3.2 y ` ¬false por ladoble negación .


2.7.19. Teorema :` (A→ false)→ ¬A

Prueba

1. {A→ false} ` A→ false Hipótesis

2. {A→ false} ` ¬false→ ¬A Contrapositiva

3. {A→ false} ` ¬false Teorema 2.3.2 , Doble Negación

4. {A→ false} ` ¬A MP 2, 3

5. ` (A→ false)→ ¬A Deducción

2.7.20. Regla de la Deducción al Absurdo :U`¬A→false

U`A .Esta es una regla muy útil (aunque controvertida) regla de la inferencia

matemática : asumir la negación de lo que usted desea probar y demostrar queconduce a una contradicción.

2.7.21. Teorema :` (A→ ¬A)→ ¬A .

Prueba

1. {A→ ¬A,¬¬A} ` ¬¬A Hipótesis

2. {A→ ¬A,¬¬A} ` A Doble Negación 1

3. {A→ ¬A,¬¬A} ` A→ ¬A Hipótesis

4. {A→ ¬A,¬¬A} ` ¬A MP 2, 3

5. {A→ ¬A,¬¬A} ` A→ (¬A→ false) Teorema 2.4.7

6. {A→ ¬A,¬¬A} ` ¬A→ false MP 2, 5

7. {A→ ¬A,¬¬A} ` false MP 4, 6

8. {A→ ¬A} ` ¬¬A→ false Deducción 8

9. {A→ ¬A} ` ¬A Reducción al Absurdo 8

10. ` (A→ ¬A)→ ¬A Deducción 9

2.7.22. Teorema :` (¬A→ A)→ A .


Estos dos teoremas puede parecer extraños, pero puede entenderseen el nivel semántico . De la implicación del teorema 2.7.22 de serfalsa, el antecedente ¬A → A debe ser true y el consecuente A false. Pero si A es falso , entonces tambien lo es ¬A → A , por lo que lafórmula es true .

2.8. Teoremas de otros operadoresHasta el momento han trabajado con la implicación como el únicooperador binario . En la sección 2.6 hablaremos de suplentes axio-maticos de Hilbert , sistemas que utilizan otros operadores, pero eneste caso que definiremos A ∧ B , A ∨ B y A ↔ B como abreviaturasde ¬ (A→ ¬B) , ¬A → B y (A→ B) ∧ (B → A) , respectivamente . Elteorema también se puede utilizar como justificación implícita paralas reglas de derivación .

2.8.1. Teorema :` A→ (B → (A ∧B)) .

Prueba

1. {A,B} ` (A→ ¬B)→ (A→ ¬B) Teorema 2.3.2

2. {A,B} ` A→ ((A→ ¬B)→ ¬B) Intercambio 1

3. {A,B} ` A Hipótesis

4. {A,B} ` (A→ ¬B)→ ¬B MP 2,3

5. {A,B} ` ¬¬B → ¬ (A→ ¬B) Contrapositiva 4

6. {A,B} ` B Hipótesis

7. {A,B} ` ¬¬B Doble Negación 6

8. {A,B} ` ¬ (A→ ¬B) MP 5, 7

9. {A} ` B → ¬ (A→ ¬B) Deducción 8

10. ` A→ (B → ¬ (A→ ¬B)) Deducción 9

11. ` A→ (B → (A ∧B)) Definición de ∧

2.8.2. Teorema : ( debilitamiento )` A→ A ∨B .

` B → A ∨B .


` (A→ B)→ ((C ∨A)→ (C ∨B)) .

Prueba (ejercicio)

2.8.3. Teorema : ( conmutatividad )` A ∨B ↔ B ∨A .

Prueba

1. {¬A→ B,¬B} ` ¬A→ B Hipótesis

2. {¬A→ B,¬B} ` ¬B → ¬¬A Contrapositiva 1

3. {¬A→ B,¬B} ` ¬B Hipótesis

4. {¬A→ B,¬B} ` ¬¬A MP 2, 3

5. {¬A→ B,¬B} ` A Doble Negación 4

6. {¬A→ B} ` ¬B → A Deducción 5

7. ` (¬A→ B)→ (¬B → A) Deducción 6

8. ` A ∨B → B ∨A Definición de ∨

9. La otra dirección es similar .

2.8.4. Teorema : ( Asociatividad )` A ∨ (B ∨ C)↔ (A ∨B) ∨ C .

Prueba

1. {¬A→ (¬B → C) ,¬ (¬A→ B)} ` ¬ (¬A→ B) Hipótesis

2. {¬A→ (¬B → C) ,¬ (¬A→ B)} ` B → (¬A→ B) Axioma 1

3. {¬A→ (¬B → C) ,¬ (¬A→ B)} ` ¬ (¬A→ B)→ ¬B Contrapositiva 2

4. {¬A→ (¬B → C) ,¬ (¬A→ B)} ` ¬B MP 1, 3

5. {¬A→ (¬B → C) ,¬ (¬A→ B)} ` A→ (¬A→ B) Teorema 3.4.7

6. {¬A→ (¬B → C) ,¬ (¬A→ B)} ` ¬ (¬A→ B)→ ¬A Contrapositiva 5

7. {¬A→ (¬B → C) ,¬ (¬A→ B)} ` ¬A MP 1, 7

8. {¬A→ (¬B → C) ,¬ (¬A→ B)} ` ¬A→ (¬B → C) Hipótesis

9. {¬A→ (¬B → C) ,¬ (¬A→ B)} ` ¬B → C MP 7, 8


10. {¬A→ (¬B → C) ,¬ (¬A→ B)} ` C MP 4, 9

11. {¬A→ (¬B → C)} ` ¬ (¬A→ B)→ C Deducción 10

12. {¬A→ (¬B → C)} ` (¬ (¬A→ B)→ C) Deducción 11

13. ` A ∨ (B ∨ C)→ (A ∨B) ∨ C Definición de ∨

14. La otra direción es similar .

Los teoremas de Conmutatividad y Asociatividad pueden ser proba-dos para ∧ y ↔ .

2.8.5. Teorema :El sistema de Hilbert H es solido , esto es , si ` A entonces |= A .

Prueba ( ejercicio )

2.8.6. Teorema :El sistema de Hilbert H es completo , esto es , si |= A entonces ` A .

2.8.7. Observación :Si un sistema deductivo es sólido , entonces ` A implica |= A , y inversamente

, 2 A implica 0 A . Por lo tanto, si hay una fórmula no válida en un sistema desólido , entonces el sistema debe ser coherente!! . Puesto que 2 false , por lasolidez de H , 0 false . Por el corolario , los axiomas de H son consistentes .

2.8.8. Teorema :U ` A si y sólo si U ∪ {¬A} es inconsistente .

2.9. Lógica Proposicional : Resolución

Una propiedad deseable de un sistema deductivo es que debe ser fácil demecanizar una búsqueda eficiente de la prueba . Es muy difícil la búsqueda deuna prueba en un sistema de Hilbert porque no hay una conexión evidente entrela fórmula y su prueba . La prueba de búsqueda en lógica proposicional es fácily eficaz con el Tableau Semántico y el equivalente (sin cortar) sistema Gentzen. Sin embargo, como veremos en el próximo capítulo, el método del Tableausemántico en lógica de predicados se convierte en arbitraria e ineficiente. Elmétodo de resolución, inventado por J. A. Robinson en 1965, es con frecuenciaun método eficaz para la búsqueda de una prueba . En esta sección, presentamosel método de la resolución para lógica proposicional, aunque sus ventajas noserán evidentes hasta que se extienda a lógica de predicados .


2.9.1. Definición :Una fórmula está en Forma Normal Conjuntiva ( FNC ) si y sólo si es la

conjunción de disyunciones de literales .

2.9.2. EjemploLa fórmula (¬p ∨ q ∨ r) ∧ (¬q ∨ r)∧(¬r) está en FNC .La fórmula (¬p ∨ q ∨ r) ∧ ((p ∧ ¬q) ∨ r)∧(¬r) no está en FNC .La fórmula (¬p ∨ q ∨ r) ∧ ¬ (¬q ∨ r)∧(¬r) no está en FNC .

2.9.3. Teorema :Toda fórmula en cálculo proposicional puede ser transformada a una fórmula

equivalente en FNC .

Prueba La conversión a una fórmula equivalente en FNC se realiza siguiendolos siguientes pasos , cada uno de los cuales preservan las equivalencias lógicas :

1. Eliminar todos los operadores excepto la negación , conjunción y disyun-ción , usando las equivalencias de 1.4.11 .

2. Las negaciones sólo afectan a átomos, utilizando las leyes de Morgan

¬ (A ∧B) ≡ ¬A ∨ ¬B¬ (A ∨B) ≡ ¬A ∧ ¬B

3. Eliminación de la doble negación usando la equivalencia ¬¬A ≡ A .

4. Eliminación de conjunciones con disyunciones , usando leyes distributivas:

A ∨ (B ∧ C) ≡ (A ∨B) ∧ (A ∨ C)

A ∧ (B ∨ C) ≡ (A ∧B) ∨ (A ∧ C)

2.9.4. Ejemplo :La siguiente secuencia de fórmulas muestra como conseguir la FNC de una

fórmula:

(¬p→ ¬q)→ (p→ q) ≡ ¬ (¬p→ ¬q) ∨ (p→ q)≡ ¬ (¬¬p ∨ ¬q) ∨ (¬p ∨ q)≡ (¬¬¬p ∧ ¬¬q) ∨ (¬p ∨ q)≡ (¬p ∧ q) ∨ (¬p ∨ q)≡ (¬p ∨ ¬p ∨ q) ∧ (q ∨ ¬p ∨ q)


2.9.5. Definición :Una cláusula es un conjunto de literales que se considera una disyunción

implícita . Una cláusula que consiste en exactamente en una literal se llamacláusula unidad . Una fórmula , en forma clausal es un conjunto de cláusulasque se considera una disyunción implícita .

2.9.6. Corolario :Toda fórmula en lógica proposicional puede ser transformada en una fórmula

en forma clausal equivalente .

2.9.7. EjemploLa fórmula en FNC (¬q ∨ ¬p ∨ q)∧ (p ∨ ¬p ∨ q ∨ p ∨ ¬p) es equivalente a la

forma clausal {{¬q,¬p, q} , {p,¬p, q}}.

2.9.8. NotaciónA veces usamos notación abreviada, eliminando el conjunto delimitado-res { y } de una cláusula y denotamos la negación con un barra sobrela letra proposicional p . La fórmula de arriba en notación abreviada es{q p q , p p q} .

Se utilizarán , los siguientes símbolos : S para un conjunto de cláusulas, C para una cláusula y l para una literal . Si l es una literal , lc es sucomplemento . El concepto de una asignación es generalizado sobre lasliterales puesto que es evidentemente : v(l) = T si y sólo si (v(p) = T yl = p) ó (v(p) = F y l = p) .

2.9.9. Definición :Sea S , S′ conjunto de cláusulas . S ≈ S′ denota que S es satisfacible si y

sólo si S′ es satisfacible .

La siguiente secuencia de lemas muestra como las fórmulas se pueden trans-formar sin cambiar su satisfacibilidad .

2.9.10. Lema :Suponga que una literal l aparece en (alguna cláusula de ) S , pero lc no

aparece en (ninguna cláusula de) S . Si S′ se obtiene de S mediante la eliminaciónde todas las cláusulas que contienen l entonces S ≈ S′.


2.9.11. Ejemplo :Sea S = {p q r , p q , p q} and S′ = {p q , p q}, donde S′ es obtenida de S

eliminando la cláusula p q r que contiene la literal l = r que aparece en S y quelc = r no aparece en S , entonces por el lema 3.2.2 S ≈ S′ . Lo que verificamos ,asignando v(p) = F , v(q) = F el cual puede ser extendida a una interpretaciónde S , asignando v(r) = T . Observe que S no es lógicamente equivalente a S′puesto que la asignación v(p) = F , v(q) = F , v(r) = T da una interpretacióna S de F a S′ de T .

2.9.12. Lema :Si C = {l } ∈ S es una cláusula unidad , si S′ se obtiene de S eliminando

todas las cláusulas que contienen l y si eliminamos lc de todas las cláusulasrestantes , entonces S ≈ S′.

2.9.13. Ejemplo :Sea S = {r , p q r , p q , q p} y S′ = {p q , p q , q p} donde {r} es la cláusula

unitaria eliminada entonces por el lema 3.2.4 S ≈ S′, lo que verificamos , asig-nando v(r) = T en algún modelo para S de modo que si v(p q r ) = T entoncescualquiera v(p) = T o v(q) = T da una interpretación a S′ de T .

2.9.14. Lema :Suponga que ambas l ∈ C y lc ∈ C para alguna C ∈ S . Si S′ = S − {C}

entonces S ≈ S′.

2.9.15. Definición :Si C1 ⊆ C2 , diremos que C1es más fuerte que C2 y C2 es más débil que C1 .

2.9.16. Lema :Sean C1, C2 ∈ S cláusulas tal que C1 es más fuerte C2 , y sea S′ = S−{C2}

. Entonces S ≈ S′, esto es , la mayor cláusula puede suprimirse .

El concepto de “es más fuerte” inicialmente puede parecer no intuitivo . Lainterpretacion que satisfaga la cláusula pequeña , también satisface la cláusulamayor.

2.9.17. Ejemplo :Sea S = {p q , p q r , p q , p q} y S′ = {p q , p q , p q} , donde p q r es más débil

que p q . Si S′ es satisfacible entonces v(p q ) = T , es evidente v(p q r ) = T .


2.9.18. Definición :La cláusula vacía es denotada por � . El conjunto vacío de cláusulas es

denotado por Ø .

2.9.19. Lema :Ø es válida , � es contradictoría .

Prueba ( ejercicio )

2.9.20. Definición :Sea S un conjunto de fórmulas y U un conjunto de letras proposicionales .

RU (S) , el cambio de nombre de S por U , es obtenido de S reemplazando cadaliteral l cuya letra proposicional se encuentra en U por lc .

2.9.21. Lema :S ≈ RU (S) .

2.9.22. Ejemplo :El conjunto de cláusulas S = {p q r , p q , q r , r }es satisfacible con la in-

terpretación v(p) = T , v(q) = F , v(r) = T . El reemplazo R{p,q}(S) ={p q r , p q , q r , r } es satisfacible con v(p) = T , v(q) = T , v(r) = T .

Resolución es una refutación al procedimiento que se utiliza parademostrar que una fórmula en forma clausal es contradictoría . Elprocedimiento resolución consiste de una secuencia de aplicaciones dela regla de resolución a un conjunto de cláusulas . La regla mantienesatisfacibilidad : si un conjunto de cláusulas es satisfacible , por lo queel conjunto de cláusulas producidas por una aplicación de la regla . Porlo tanto, si la cláusula contradictoría vacía es obtenido cada cadavez, el conjunto original de cláusulas debe haber sido contradictoría .

2.9.23. Regla de ResoluciónSea C1 , C2cláusulas tales que l ∈ C1 , lc ∈ C2 . Las cláusulas C1 , C2

se dice que colisionan y que colisionan en las literales complementarias l , lc. La cláusula resolvente de C1 y C2 , es la cláusula : C = Res(C1, C2) =(C1 − {l }) ∪ (C2 − {lc}) .

Diremos que ,C1 y C2 son cláusulas padre de C .


2.9.24. Ejemplo :El par de cláusulas C1 = a b c y C2 = b c e colisionan en el par c , c la

resolvente es C = (a b c− {c } ∪ b c e− {c}) = abe .

2.9.25. Teorema :La resolvente C es satisfacible si y sólo si las cláusulas padre C1 y C2 son

mutuamente satisfacibles .

2.9.26. Algoritmo :Entrada : Un conjunto de cláusulas S

Salida : S es satisfacible o contradictoria

1. Defina S0 = S

2. Suponga que Si ha sido construida . Elija un par de cláusulas que colisionenC1, C2 ∈ Si que no hayan sido elegidas antes . Defina C = Res(C1, C2) ,Si+1 = Si ∪ {C }.

a) Si C = � termina el procedimiento y S es contradictoria .

b) Si Si+1 = Si para todas las opciones posibles cláusulas de colisión ,termina el procedimiento y S es satisfacible .

2.9.27. Ejemplo :Sea S = {(1) p , (2) p q , (3) r , (4) p q r} donde las cláusulas estan numeradas

para referencia .

1. S0 = {(1) p , (2) p q , (3) r , (4) p q r}

2. S1 = {(1) p , (2) p q , (3) r , (4) p q r , (5) p q } 3,4

3. S2 = {(1) p , (2) p q , (3) r , (4) p q r , (5) p q , (6) p} 2,5

4. C = � 1,6

Por lo tanto , S es contradictoría .

Es más fácil de leer la resolución , si se presenta como un árbol de derivación, donde las cláusulas originales son las etiquetas de las hojas, y las resolventesetiquetan nodos interiores, cuyos hijos son las cláusulas utilizadas en la resolu-ción


�↙ ↘

p p↙ ↘

p q p q↙ ↘

p q r r

En el ejemplo , hemos obtenido la cláusula contradictoría � que nos permi-te concluir que el conjunto de cláusulas S es contradictoría . Dejamos para ellector comprobar que S es la forma de clausal de ¬A donde A es una instanciadel Axioma 2 de H : (p→ (q → r)) → ((p→ q)→ (p→ r)). Por lo tanto, ¬Aes contradictoría, esto es A es válida y que hemos utilizado la resolución parademostrar que esta instancia de Axioma 2 es válida .

2.9.28. Definición :La derivación de � desde S es llamada una refutación de S .

2.9.29. Teorema :Si el conjunto de cláusulas de etiquetado de las hojas de un árbol de la

resolución es satisfacible entonces la cláusula en la raíz es satisfacible .

2.9.30. ObservaciónEl reciproco del teorema 3.3.8 no necesariamente es verdadero porque no

tenemos manera de asegurar que las extensiones hechas a v en todas las ramasson consistentes . En la figura, el conjunto de cláusulas en las hojas del árbol{r , p q r , r , p q r} no es satisfiable a pesar de que la cláusula relativa a la raízp es satisfiable.

p↙ ↘

p q p q↙ ↘ ↙ ↘

p q r r p q r r

2.9.31. Corolario : (Solidez )Si la cláusula vacia � es derivada de un conjunto de cláusulas por la pro-

cedimiento de resolucion , entonces el conjunto de cláusulas es contradictoria.

2.9.32. Teorema : ( Compleción)Si un conjunto de cláusulas es contradictoria entonces la cláusula vacía � se

obtendrá por el procedimiento de resolución .


Tenemos que demostrar , que dado un conjunto de cláusulas contradictoria, el procedimiento de resolución a la larga termina produciendo � , en lugarde continuar indefinidamente o que termine y no produzca �. Hemos definidoel procedimiento de resolución como un procedimiento sistemático en el que unpar de cláusulas nunca es elegido más de una vez . Dado que sólo hay un númerofinito de distintas cláusulas , con un conjunto finito de letras proposicionales ,el procedimiento termina. Por lo tanto, sólo tenemos que demostrar que cuandotermina el procedimiento, produce la cláusula vacía .

2.10. Semánticas y Lenguajes de Programa-ción

Un lenguaje de programación puede considerarse que es un lenguaje formaldesde el momento que su sintaxis y su semánticaf están definidas formalmente.La primera se ocupa de fijar las reglas que describen las estructuras sintácticas(formalmente correctas) que constituyen los programas, es decir, la forma delas instrucciones, las declaraciones, las expresiones aritméticas y otras construc-ciones del lenguaje. La teoría de Autómatas y Lenguajes Formales proporcio-na herramientas para la definición sintáctica de los lenguajes de programación(grámaticas, notaciones, etc). Respecto a la semántica, las distintas “escuelas”o familias de lenguajes se diferencian en la forma con la que enfocan la descrip-ción de los aspectos semánticos dependiendo de su uso y de la riqueza que sepretende alcanzar en la descripción: operacional; axiomático o declarativo (consus diversas orientaciones) son los más representativos.

2.10.1. Necesidad de una Definición Semántica FormalSi bien la definición sintáctica de un lenguaje de programación mediante una

grámatica formal, por ejemplo en notación BNF, facilita su análisis sintático,ésta no es suficiente para la comprensión de sus estructuras sintácticas. Puedeocurrir que ciertas restricciones del lenguaje no son expresables en BNF y portanto, forman parte de la descripción semántica del lenguaje, en la mayoria delos manuales y libros que describen un lenguaje de programación, es habitualorganizar la descripción del lenguaje alrededor de la diversas estructuras sintá-ticas que posee. En estos manuales se define la sintaxis de una construcción yse pasa a dar el significado de la misma indicando sus características de fun-cionamiento mediante el empleo de un lenguaje natural (español, inglés, etc)Podriamos denominar semántica informal a esta forma de descripción. La defi-nición semántica mediante el lenguaje natural (en apoyo de las producciones enBNF o cualquier otra forma de expresar la sintaxis) encierra ambigüedades y enocasiones las descripciones empleadas no suelen ser lo suficientemente precisascomo para captar todos los matices del significado de una construcción. Estopuede conducir a errores de programación y a, lo que es aún peor, errores de


implementación cuandos se utiliza una semántica informal como base para ladescripción del propio lenguaje.

Otra forma de dar significado a los lenguajes de programación ha sido lallamada semántica por traducción, que consiste en definir el significado de unlenguaje por medio de la traducción de sus construcciones sintácticas a un len-guaje ya conocido. Esto puede hacerse bien por una técnica de interpretacióno de compilación. Si disponemos de una máquina concreta M cuyo conjuntode instrucciones y funcionamiento es conocido, un compilador que transformeprogramas escritos en nuestro lenguaje de programación (lenguaje fuente) enprogramas del lenguaje de la máquina M (lenguaje objeto) sería una definiciónsemántica del lenguaje que nos permite definir el significado de los programasdel lenguaje de programación como el programa obtenido tras la compilación.Sin embargo un interprete o un compilador no se consideran propiamente defini-ciones semánticas ya que este tipo de definiciones prersentan varios problemas:

1. Definir las instrucciones del lenguaje en términos de las de una máquinareal M aporta un grado de complejidad que no está presente en el propiolenguaje sino en el modelo elegido para su representación. Esto conduce auna falta de abstracción en la descripción semántica, que se pierde en losdetalles.

2. La falta de portabilidad sería otro de los problemas. En este caso la defi-nición semántica depende de la máquina M escogida. Claramente, si cam-biamos a una máquina M’, el traductor deberá reescribirse en términos dellenguaje de máquina de M’ o la máquina M deberá simularse en términosde la de M’.

3. Una de las aplicaciones de las definiciones semánticas es servir de ayudaa la construcción de traductores de lenguajes, así pues, esta orientaciónsubvertiría uno de sus objetivos.

Los dos primeros problemas pueden suavisarse si definimos una máquina virtual,más abstracta, que sea fácil y eficientemente simulada por las máquinas realescon distintos conjuntos de instrucciones. Dicha máquina sería una abstracciónde las características presentes en todas ellas. El conjunto de instrucciones dela máquina virtual permitiría definir un código intermedio como resultado de lacompilación del lenguaje fuente3 . Sin embargo, dependiendo el nivel de abstrac-ción, la definición podría no servir para algunos usos pretendidos de la misma.La discusión precedente sugiere la necesidad de dotar a los lenguajes de pro-gramación de una semántica formal, para asegurar que las definiciones de lasconstrucciones del lenguaje sean claras y evitar ambigúedades en su interpreta-ción.

Las semánticas formales se definen mediante:

Una descripción formal de la clase de objetos que pueden manipularse porlas construcciones del lenguaje. Estos objetos pueden ser: estados de una

3Esta solución, introducida en los años 70 en los lenguajes Pascal y Prolog, ha sido adoptadaen la implementación del lenguaje Java para aumentar su portabilidad.


máquina (abstracta), funciones, valores, asertos u otra clase de objetosque deberán especificarse formalemente.

Un conjunto de reglas que describen las distintas formas en que las expre-siones del lenguaje adquieren significado y pueden combinarse para dar lasalida (asociada a cada una de las expresiones compuestas) en términosde sus constituyentes.

Al dotarnos de una semántica formal para un lenguaje de programación que-remos construir un modelo matemático que nos permita comprender y razonarsobre el comportamiento de los programas, así como construir herramientas úti-les para su manipulación automática (transformación, verificación, depuración,etc). También queremos establecer con precisión criterios para comprobar laequivalencia entre programas. Esto es de singular importancia, entre otras co-sas, en el estudio de técnicas de transformación de programas, en las que sepretende establecer la equivalencia entre el programa original y el transformadocomo una simple consecuencia de la corrección y completitud del método detransformación.

2.10.2. Semánticas Formales de los Lenguajes deProgramación

Debido al hecho de que se requiere estudiar las características de los lenguajesde programación con distintos niveles de detalle y diferentes perspectivas, se hanpropuesto diversas aproximaciones a la semántica formal de los lenguajes deprogramación. Aquí describimos sucintamente algunas de las más importantes.

2.10.2.1. Semántica Operacional

Es el enfoque más antiguo de la definición semántica formal de un lenguaje( con este estilo se definió la semántica del ALGOL’60 ). La semántica ope-racional proporciona una definición del lenguaje en términos de una máquinaabstracta (de estados). La idea es sencilla, debemos de dar una noción de es-tado abstractoque contenga la información esencial para describir el proceso deejecución de un programa del lenguaje en esa máquina. Entoces, la semánticade un lenguaje de programación se define indicuando cuál es el efecto de lasconstrucciones sintácitcas del lenguaje sobre el estado de la máquina abstracta.Esto es, el significado de una instrucción se define en términos del cambio deestado (abstracto) que produce cuando se ejecuta. Intuitivamente, la semánticaoperacional equivale a la definición de un intérprete (abstracto) para el lenguaje,que lo hace ejecutable.

A menudo, la especificación operacional de un lenguaje de programación selleva a cabo mediante el uso de sistemas de transición y las distintas fases porlas que atraviesa la ejecución de un programa se presentan mediante diferentessconfiguraciones de la máquina abstracta.


2.10.2.2. Semántica Axiomática

Este es el enfoque típico de los trabajos sobre verificación formal de progra-mas imperativos. Con este estilo se definio la semántica del lenguaje Pascal. Laidea básica consiste en definir el significado de un programa como la relaciónexixtente entre las propiedades que verifica su entrada (precondiciones) y laspropiedades que verifica su salida (postcondiciones) . Las precondiciones y laspostcondiciones son fórmulas de algún sistema lógicoque especifican el signifi-cado del programa. Dichas fórmulas pueden ser enunciados sobre el estado dela computación, pero no necesariamente debe ser así. Por ejemplo, la semán-tica axiomática de un programa que calcula el cociente C y resto R de dosenteros X e Y vendría definida por la precondición {Y ≥ 0} y la postcondición{X = Y ∗ C +R}. Como se ha dicho, la semántica axiomática se emplea prin-cipalmente en tareas de verificación de programas y suele emplearse la notación{P}C {Q}, que indica que si el enunciado P (precondicción) es verdadero an-tes de la ejecución del código C, entonces el enunciado Q (postcondición) esverdadero despues de su ejecución (supuesto que la ejecución de C termina) .La semántica axiomática utiliza las reglas de inferencia de la lógica de predica-dos introduciendo además otras reglas de inferencia adicionales que establecenel significado de cada estructura sintáctica del lenguaje (asignación, condicio-nal,iteración, etc.).

Habitualmente la verificación de programas procede hacia atras (backward)en el código: conocida la postcondición de una instrucción, se deriva que pre-condición debe de ser cierta antes de su ejecución para asegurar lo que es ciertodespués (caracterizado por la popstcondición); en concreto se calcula la pre-condición más débil que garantiza el tránsito al estado caracterizado por lapostcondición.

Empleando esta técnica se puede verificar, no sin dificultad la correcciónde pequeños programas imperativos: basta comprobar que la precondicción delprograma implica la precondición más débil que se obtiene para la primerainstrucción del programa (la última en procesarse ya que el método parte dela postcondición). Sin embargo, hay que admitir que cuando el tamaño de losprogramas es considerable esta técnica se torna impracticable. Esta dificultadtambién puede verse como un reflejo de la propia complejidad de los lenguajesimperativos.

2.10.2.3. Semántica Declarativa

En esta clase de semánticas el significado de cada construcción sintáctica sedefine en términos de elementos y estructuras de un dominio matemático cono-cido. Dependiendo del dominio escogido, este enfoque ha dado lugar a diferentesaproximaciones:

1. Semántica por teoría de modelos

Esta aproximación está basada en la semántica de la lógica de predicadosque estudiaremos en el siguiente cápitulo. Con este estilo se ha definido lasemántica de lenguajes de programación lógica como Prolog.


2. Semántica algebraica

Esta aproximación está basada en la teoría de álgebras libres. Con esteestilo se ha definido la semántica de lenguajes ecuacionales de primer or-den, una calse especial de lenguajes funcionales donde los programas sonconjuntos de ecuaciones entre términos que definen funciones. En ellos unprograma se interpreta haciendo uso de nociones algebraicas como álgebracociente y álgebra modelo de un conjunto de ecuaciones. También se hautilizado para definir la semántica de los lenguajes de especificación detipos abstractos de datos como OBJ.

3. Semántica de punto fijo

Esta aproximación está basada en la teoría de las funciones recursivas.Generalmente se utiliza como enlace para demostrar la equivalencia entrediferentes caracterizaciones semánticas de un mismo lenguaje. Se asocia alprograma un operador (generalmente continuo) que opera sobre el dominiode interpretación, de manera que el significado del programa se define comoel (menor) punto fijo de dicho operador. Con este enfoque seha definidola semántica de los lenguajes lógicos.

4. Semántica denotacional

Esta aproximación está basada en la teoría de dominios. La idea fundamen-tal de este tipo de semánticas es interpretar las construcciones sintácticasde un lenguaje como valores de un determinado dominio4 matemático.La semántica denotacional de un programa viene dada por la función queéste denota. La semántica denotacional se centra en “lo esencial” de lacomputación, es decir en el resultado final obtenido. Asípues la semánticadenotacional posee un grado de abstracción mayor que el de la semánticaoperacional, ya que no se fija en los estados intermedios (de una máquinaabstracta) generados durante la ejecución de un programa, lo único impor-tante son las funciones asociadas a los programas, no cómo se construyen;en cambio, en una semántica operacional los estados intermedios formanparte de la definición. Informalmente, podemos decir que la semántica de-notacional es más declarativa que la semantica operacional.Técnicamente, la semantica denotacional es generalmente la más comple-ja de las caraterizaciones semánticas, si bien es muy rica, ya que permitedar cuenta de computaciones que no terminan y del orden superior en loslenguajes de programcaión . Para su definición se requiere describir :

a) Por cada construcción sintáctica un dominio sintático; en general,tendrán que definirse dominios sintáticos para los identificadores, lasconstantes, los operadores, las expresiones, las instrucciones (o fór-mulas) y los programas.

4La palabra “dominio” se emplea con una connotación más rica que la empleada en la teoríade modelos de la lógica de predicados (y también en otras aproximaciones) . En la teoría demodelos, un dominio es un conjunto simple, sin ningín tipo de estructura. En el ámbito de lasemántica denotacional, un dominio es un conjunto dotado de una estructura más elaboradaque se caracteriza por poseer, al menos, un orden parcial completo con un elemento mínimo.


b) Los dominios semánticos; uno por cada dominio sintáctico identifica-do.

c) Las funciones de evaluación semántica, de los dominios sintáticos alos semánticos, que asocian a cada construcción sintáctica su valorsemántico.

d) Un conjunto de ecuaciones semánticas. Una característica importantede las descripciones denotacionaleses que las funciones de evaluación-semántica vienen definidas por inducción sobre la estructura de lasexpresiones. Esto da lugar a un estilo de definición composicionaldonde el valor de una estructura sintáctica queda queda completa-mente determinado en función del valor sus componentes.

Con este estilo se ha definido la semántica declarativa de la mayoría de loslenguajes funcionales (Haskell, ML) así como la del lenguaje imperativoADA.

2.11. Lista de Ejercicios1. ¿Cuál de las siguientes afirmaciones, relativas al cálculo deductivo de un

sistema formal, es cierta?

a) Permite deducir nuevas fbf teniendo en cuenta aspectos sintácticos ysemánticos .

b) Tiene que ver con la definición axiomática de una serie de estructurasinductivas correctas y las reglas para obtener otras nuevas a partirde aquéllas.

c) No tiene en cuenta la interpretación de los símbolos del formalismoni el significado de las fbf.

2. Un sistema formal es correcto si:

a) Toda fórmula demostrable mediante el cálculo deductivo es válidasegún la noción de verdad de la semántica.

b) Toda fórmula semánticamente válida es demostrable mediante el cálcu-lo deductivo.

c) Existe un procedimiento finito para decidir si una fórmula es o noválida.

d) Su método de cálculo es el dela lógica de predicados de primer orden.

Seleccione la respuesta correcta de entre las anteriores.

3. Indique cuál de las siguientes afirmaciones es falsa:

a) En un sistema formal los símbolos carecen de significado.


b) Una fórmula bien formada es cualquier cadena de símbolos que tienesignificado completo.

c) La teoría de la demostración estudia los formalismos con indepen-dencia de toda interpretación.

4. Ecribir el árbol de formación y la tabla de verdad de (p→ (q → r)) →((p→ q)→ (p→ r)).

5. Demostrar que :A ∨B ≡ ¬ (¬A ∧ ¬B).

6. Demostrar que si U es satisfacible entonces U ∪{B} no nesarariamente essatisfacible.

7. Analizar la validez de la fórmula A utilizando el método del Tableau se-mántico

a) A = (¬p ∧ q) ∧ (((r → p)↔ ¬q) ∨ ¬r) ∧ ¬ (r ∨ ¬p)b) A = {(p ∧ r) ∨ ¬r → q , (q ↔ r)→ (¬q → r) , (¬p ∧ q) ∧ ¬r }

8. Considere el conjunto U = {p ∨ q → r ∨ s , r ∧ t→ s , r ∧ ¬t→ ¬u}. De-cide, usando el Tableau semántico si U |= p→ s ∨ ¬u .

9. Provar que |= (p→ r) → ((q → r)→ (p ∨ q → r)) usando el Tableau se-mántico .

10. Demostrar que : {p→ ¬q , r → q} |= ¬ (p ∧ r).

11. Dada la fórmula A = (¬p→ (q → (p ∧ r)))→ (¬p ∧ r) .

a) Usa el método del Tableau semántico para clasificar la validez de A .

b) Si existen , halla un modelo y un contrajemplo para A .

12. Dada la fórmula A = (¬p→ (q → (p ∧ r)))→ (¬p ∧ r) .

a) Usa el método del Tableau semántico para clasificar la validez de A .

b) Si existen , halla un modelo y un contrajemplo para A .

13. Probar en G : ` (A→ B)→ (¬B → ¬A).

14. Provar en G : ` (A→ B)→ ((¬A→ B)→ B).

15. Probar en H : ` (A→ B)→ ((¬A→ B)→ B).

16. Provar en H : ` (A→ B)→ ((C ∨A)→ (C ∨B)).

17. Construir un Tableau semántico para mostrar que el axioma 2 de H esválida .

18. Probar la regla derivada llamada Modus Tollens : `¬B `A→B`¬A


19. Probar que si U es un conjunto de fórmulas válidas y A es una fórmulatal que U |= A entonces A es válida .

20. Transforma el conjunto de fórmulas en la forma clausal y refute usandoresolución{p , p→ ((q ∨ r) ∧ ¬ (q ∧ r)) , p→ ((s ∨ t) ∧ ¬ (s ∧ t)) , s→ q , ¬r → t , t→ s }.

21. Los lenguajes imperativos no sirven como lengaujes de especificación por-que:

a) No tienen una sintaxis y una semántica bien definidas.

b) Introducen detalles que no son característicos del problema sino dela solución encontrada.

c) No tienen una base lógica.

d) No son ejecutables.


22. Indique cuál de las siguientes sentencias es falsa:

a) La semántica denotacional proporciona una definición del lenguajeen términos de una máquina abstracta (de estados).

b) Las semánticas formales facilitan las tareas de análisis y verificaciónde programas.

c) En la semántica por traducción el significado del programa (fuente)es el mismo que el del programa obtenido tras la compilación.

23. Describa las principales características de la semántica operacional.

24. Indique qué elección para la definición semántica de un lenguaje de pro-gramación resultaría apropiada, si quisieramos emplearla como ayuda ...

a) ... a la programación: Semántica por punto fijo.

b) ... a la implementación de un lenguaje: Semántica operacional.

c) ... a las pruebas de equivalencia entre semánticas: Semántica axiomá-tica.

d) ... a la modelización con un lenguaje imperativo: Semántica por teoríade modelos.

25. Para la descripción de los aspectos semánticos de un lenguaje de progra-mación con un enfoque operacional:

a) Se define el significado de cada construcción del lenguaje como elobjeto que dicha construcción denota.


b) Se define una máquina abstracta y se expresa el significado de ca-da construcción del lenguaje en función de las diferentes acciones arealizar por la máquina para su ejecución.

c) Se define el significado de cada construcción del lenguaje por mediode axiomas que establecen lo que se puede afirmar sobre el estadodel programa tras su ejecución, en función de lo que era verdaderoantes, o viceversa.

d) Se define el significado de cada construcción del lenguaje como elpunto fijo de una función continua y monótona definida para el pro-grama.


26. Explique con precisión que se entiende por lenguaje de programación de-clarativa. Indique sus principales características (entendido como sistemaformal). Hable de su semántica operacional y declarativa y de la relaciónexistente entre ambas.

27. Genéricamente, la programación declarativa puede entenderse como:

a) Única y exclusivamente, programación con cláusulas de Horn defini-das.

b) Cualquier paradigma de programación en que los conceptos de compu-tación en la máquina, deducción en una lógica apropiada y satisfac-ción en un modelo estándar del programa resultan equivalentes.

c) Una metodología de progamación con diagramas lógicos.

d) Lo contrario de la programación natural.


Parte III

Lógicas

88

Capítulo 3

Lógica de Predicados :Fórmulas , Modelos y Tableau

3.1. IntroducciónEl cálculo proposicional no es lo suficientemente expresivo para lasteorías matemáticas, tales como la aritmética. Una expresión arit-mética como x > y no es ni verdadero ni falso. Su valor de verdaddepende de los valores de x y y ; más formalmente, el operador > esuna función de pares de números enteros (o números reales) hacia elconjunto de valores booleanos {true , false }. El sistema de lógica queincluye funciones de dominios tales como números a valores booleanosse llama cálculo de predicado o lógica de primer orden . El cálculode predicados es suficiente para la mayoria de las aplicaciones de lalógica a las matematicas , tales como la formalización de la aritméticay el álgebra . Similarmente , la mayoria de las aplicaciones de la ló-gica a la ciencia de la computación usa el cálculo de predicados o unsistema lógico que puede ser formulado en el cálculo de predicados .

Un uso muy importante del cálculo de predicados es formalizar la se-mántica de los lenguajes de programación , para especificar y verificarlos programas. En primer lugar tengamos en cuenta que la sintaxisde un lenguaje de programación se especifica por una gramática, unconjunto de reglas para la construcción de programas sintácticamentelegales .

3.1.1. Ejemplo :Habida cuenta de la declaración

89

CAPÍTULO 3. LÓGICA DE PREDICADOS :FÓRMULAS , MODELOS Y TABLEAU90

if x >= 0 then y :=sqrt(x) else y := abs(x)

Podemos darnos una fórmula en el cálculo de predicados en x ’ yy’ (los valores de x, y después de la ejecución de la declaración) quese refieren a x , y (los valores de x, y antes de la ejecución de ladeclaración):∀x ∀y (x′ = x ∧ (x >= 0→ y′ =

√x ) ∧ (¬ (x >= 0)→ y′ = |x |))

La fórmula x’ = x especifica que el valor de x no cambia durante laejecución de la declaración.

3.2. Relaciones y PredicadosLos axiomas y teoremas de matemáticas son definidos sobre un con-junto arbitrario , como el conjunto de los enteros Z . Tenemos queser capaces de escribir y manipular fórmulas lógicas que contienensus valores en las relaciones arbitrarias de conjuntos . El cálculo depredicados es una extensión del cálculo proposicional , los predicadosson letras que se interpretan como relaciones en un dominio.

Sea R una relación n − aria sobre el dominio D , es decir , R es unsubconjunto de Dn .

3.2.1. Ejemplo :Pr(x) ⊂ N es el conjunto de los números primos {2, 3, 5, 7, 11, · · ·} .

Sq(x, y) ⊂ N2 es el conjunto de pares (x, y) tal que y = x2 : {(0, 0) , (1, 1) , (2, 4) , (3, 9) , · · ·}.

3.2.2. Definición :Una relación puede ser representado por una función de valores boo-leanos R : Dn → {T, F }, definida por : R(d1, d2, · · · , dn) = T si y sólo si(d1, d2, · · · , dn) ∈ R .

3.2.3. Ejemplo :Sq y Pr son representadas por las funciones Sq y Pr , respectivamente:

Pr(0)=F Pr(1)=F Pr(2)=T · · ·


Sq(0,0)=T Sq(0,1)=F Sq(0,2)=F · · ·Sq(1,0)=F Sq(1,1)=T Sq(1,2)=F · · ·Sq(2,0)=F Sq(2,1)=F Sq(2,2)=F · · ·

......

......

Esta correspondencia es trivial pero proporciona el vínculo necesariopara una formalización lógica de la matemática . Todos los mecanis-mos de la lógica - las fórmulas, las interpretaciones, pruebas, etc - quehemos desarrollado para el cálculo proposicional pueden ser aplicadosal cálculo de predicados. La presencia de un dominio en el cálculo depredicados complica considerablemente los detalles técnicos pero nolos conceptos básicos .

Una visión general :

Sintaxis : Letras de predicados son usadas para representar relaciones (funciones de un dominio hacia valores de verdad ) . Los cuantificadoresson expresiones puramente sintácticas , que declaran que la relación re-presentada por un predicado es verdadera para algunos o para todos loselementos en un dominio .

Semántica: Una interpretación consiste de un dominio y de una asignaciónde las relaciones subyacentes a las letras de predicado . La semántica delos operadores booleanos se mantienen sin cambios, pero la evaluación delos valores verdad de una fórmula deben tener cuenta los cuantificadores .

Tableau Semántico : La búsqueda sistemática en un modelo es poten-cialmente infinita porque los dominios de los enteros son infinitos . Laconstrucción de un tableau puede no terminar, por lo que no hay un pro-cedimiento para la decisión de satisfacibilidad en el cálculo de predicados. Sin embargo, si ocurre un tableau cerrado , la fórmula es contradictoria, por el contrario, si la fórmula es contradictoria el tableau es cerrado .

En los sistemas deductivos de Gentzen y Hilbert que son sólidos y comple-tos . Una fórmula válida es demostrable y podemos construir una pruebade la fórmula utilizando tableaus , pero dada una fórmula arbitraria nopodemos decidir si es válida y, por tanto, demostrable .

La sintaxis del cálculo de predicados es una extensión de las letras defunción que se interpretan como funciones sobre el dominio. Con funcio-nes podemos razonar acerca de las operaciones matemáticas, por ejemplo(x > 0 ∧ y > 0 ) → (x y > 0). El cálculo de predicados con letras de fun-ción se utiliza en el procedimiento de resolución que veremos mas adelante.


3.2.4. Fórmulas en Cálculo de PredicadosSea P ,A y V conjuntos contables de símbolos llamados letras depredicados , constantes y variables respectivamente . Por convención,P = {p, q, r} , A = {a, b, c} , V = {x, y, z}, posiblemente con subíndices,indican estos conjuntos .

3.2.5. Definición :La siguiente gramática define fórmulas atomincas y fórmulas en lecálculo de predicados :

1. argument ::= x para toda x ∈ V

2. argument ::= a para toda a ∈ A

3. argumet−list ::= argument

4. argumet−list ::= argument , argument−list

5. atomic−formula ::= p | p (argument−list) para todo p ∈ P

6. formula ::= atomic−formula

7. formula ::= ¬formula

8. formula ::= formula ∨ formula

9. formula ::= formula ∧ formula

10. formula ::= formula → formula

11. formula ::= formula ↔ formula

12. formula ::= formula ⊕ formula

13. formula ::= formula ↑ formula

14. formula ::= formula ↓ formula

15. formula ::= ∀x formula para toda x ∈ V

16. formula ::= ∃x formula para toda x ∈ V

Una letra de predicado p ∈ P puede no tener argumentos o teneralgún número finito de argumentos . Consideramos que dos letras depredicados con diferentes aridades , como distintas .

La definición de la derivación , de los árboles de formación , y elconcepto de inducción sobre la estructura de una fórmula se hace sincambios desde el cálculo proposicional. Los cuantificadores se consi-deran con mayor precedencia que los operadores booleanos .


3.2.6. Ejemplo :He aquí algunas fórmulas en cálculo de predicados :

1. ∀x∀y (p (x, y)→ p (y, x))

2. ∀x∃y p (x, y)

3. ∃x∃y (p (x) ∧ ¬p (y))

4. ∀x p (a, x)

5. ∀x (p (x) ∧ q(x))↔ (∀x p (x) ∧ ∀x q(x))

6. ∃x (p (x) ∨ q(x))↔ (∃x p (x) ∨ ∃x q(x))

7. ∀x (p (x)→ q(x))→ (∀x p (x)→ ∀x q(x))

8. (∀x p (x)→ ∀x q(x))→ ∀x (p (x)→ q(x))

3.2.7. Definición :∀ es el cuantificador universal y se lee “para todo” . ∃ es el cuantificadorexistencial y se lee “existe” . En la fórmula cuantificada ∀xA , x es lavariable cuantificada y A es el ambito de la variable cuantificada . Noes necesario que x aparezca en el ámbito de su cuantificación .

3.2.8. Definición :Sea A una fórmula . La variable x en A es una variable es libre siy sólo si no esta en el ámbito de algún cuantificador . Notación :A (x1, · · · , xn) indica que el conjunto de variables libres de la fórmulaA es un subconjunto de {x1, · · · , xn}. Una variable que no es libre sedice que está ligada .

Si una fórmula no tiene variables libres , se dice que es cerrada . Si{x1, · · · , xn}son todas variables libres de A , la clausura universal de Aes ∀x1 · · · ∀xnA y la clausura existencial es ∃x1 · · · ∃xnA .

3.2.9. Ejemplo :p (x, y) tiene dos variables libres x y y , ∃yp (x, y) tiene una variablelibre y una ligada .∀x∃y p (x, y) es cerrada . La clausura universal dep (x, y) es ∀x∀y p (x, y) y la clausura existencial es ∃x∃y p (x, y) .


3.2.10. Ejemplo :En la fórmula ∀x p(x) ∧ q(x) , la ocurrencia de x en p(x) es ligada y laocurrencia en q(x) es libre . La clausura universal es ∀x(∀x p(x)∧q(x)) .Evidentemente , habría sido mejor escribir la fórmula como ∀x p(x) ∧q(y) donde y es una variable libre ; así su clausura es ∀y(∀x p(x)∧ q(y)).

3.3. Interpretaciones

3.3.1. Definición :Sea U un conjunto de fórmulas tales que {p1, · · · , pn} son letras depredicados y {a1, · · · , ak} son las constantes que aparecen U . Unainterpretación I es una tripla (D, {R1, · · · , Rm} , {d1, · · · , dk}) , donde Dun dominio no vacio , Ri es una asignación de una relación ni − ariasobre D a la ni − aria letra de predicado pi y di ∈ D es una asignacionde un elemento de D a la constante ai .

3.3.2. Ejemplo :Lo que sigue, son interpretaciones numéricas para la fórmula ∀x p (a, x): I1 = (N, {≤} , {0}) , I2 = (N, {≤} , {1}), I3 = (Z, {≤} , {0}) .

La fórmula puede también interpretarse sobre Strings I4 = (S, {substr} , {” ”}), donde S es el conjunto de Strings sobre algún alfabeto , substr es larelacion binaria substring y ” ” es el String vacio .

3.3.3. Definición :Sea I una interpretación . Una asignación σI : V 7→ D es una funciónque asigna a toda variable un elemento del dominio de I . σI [xi ← di]es una asignación que es la misma que σI excepto que xi es asignadaa di .

3.3.4. Definición :Sea A una fórmula , I una interpretación y σI una asignación . vσI

(A), es el valor de A a travéz de la asignación σI , que es definida porinducción sobre la estructura de A :

Sea A = pk(c1, · · · , cn) una fórmula atómica donde cada ci es cualquiervariable xi o una constante ai . vσI

(A) = T si y sólo si {d1, · · · , dn} ∈ Rkdonde Rk es la relación asignada por I a pk , y di es el elemento deldominio asignado a ci , ya sea por I si ci es una constante o por σI si cies una variable .


vσI(¬A1) = T si y sólo si vσI

(A1) = F

vσI(A1 ∨ A2) = T si y sólo si vσI

(A1) = T o vσI(A2) = T y similarmente

para todos los demás operadores booleanos .

vσI(∀xA1) = T si y sólo si vσI [x←d](A1) = T para todo d ∈ D .

vσI(∃xA1) = T si y sólo si vσI [x←d](A1) = T para algún d ∈ D .

3.3.5. Teorema :Sea A una fórmula cerrada . Entonces vσI

(A) no depende de σI .

Por el teorema , podemos hablar del valor de una fórmula cerrada, denotada por vI(A) , sin mencionar una asignación especifica . Dehecho, muy raramente hay alguna necesidad de considerar fórmulasno cerradas por el siguiente teorema .

3.3.6. Teorema :Sea A′ = A (x1, · · · , xn) una fórmula no cerrada y sea I una interpreta-ción , entonces :

vσI(A′) = T para alguna asignación σI si y sólo si vI (∃x1 · · · ∃xnA′) = T

.

vσI(A′) = T para todas las asignaciones σI si y sólo si vI (∀x1 · · · ∀xnA′) =

T .

3.3.7. Definición :Una fórmula cerrada A es verdadera en I o I es un modelo de A , sivI(A) = T . Notación : I � A .

3.3.8. Ejemplo :Para la fórmula ∀x p (a, x) y la interpretación definida arriba :

I1 � A puesto que , para todo n ∈ N , 0 ≤ n .

I2 2 A puesto que , no es verdadero que para todos los n ∈ N , 1 ≤ n . Sin = 0 entonces 1 � 0 .

I3 2 A porque no existe entero más pequeño .

3.3.9. Definición :Una fórmula cerrada A es satisfacible si para alguna interpretación I, I � A . A es válida si para toda interpretación I , I � A . Notación :� A . A es contradictoria si no es satisfasible , y es falsifiable si es noválida .


En adelante , cuando hablemos de la satisfacibilidad o validez de unafórmula, la hipótesis es que la fórmula es cerrada aunque no lo men-cionemos explícitamente.

3.3.10. Ejemplo :∀x p(x) → p(a) es válida . Si no es así, debe haber una interpretaciónI = (D, {R} , {d})tal que vI(p(a)) = F y vσI

(p(x)) = T para todas laasignaciones σI , en particular para la asignación σ′I que asigna a a x .Pero p(a) es cerrada ,entonces vσ′

I(p(a)) = vI(p(a)) = T , lo cual es una

contradicción .

3.3.11. Ejemplo :Lo que sigue es un análisis semántico de las fórmulas del ejemplo 4.1.6

1. ∀x∀y (p (x, y)→ p (y, x))

La fórmula es satisfacible en una interpretación donde a p se le asignauna relación simetrica como = .

2. ∀x∃y p (x, y)

La fórmula es satisfacible en una interpretación donde a p se le asignauna relación que es una función total , tal como (x, y) ∈ R sii y =x+ 1 para x, y ∈ Z .

3. ∃x∃y (p (x) ∧ ¬p (y))

Esta fórmula es satisfacible solamente en un dominio con al menosdos elementos .

4. ∀x p (a, x)

Esto expresa la existencia de un elemento especial. Por ejemplo , sip es interpretada por la relación ≤ sobre el dominio de N , entoncesla fórmula es verdadera para a = 0 . Si cambiamos el dominio a Zla fórmula es falsa para alguna asignación de ≤ a p . Así pues, uncambio de dominio por sí solo puede cambiar la satifacibilidad de unafórmula .

5. ∀x (p (x) ∧ q(x))↔ (∀x p (x) ∧ ∀x q(x))

La fórmula es válida . Demostraremos la dirección hacia adelante →y dejamos como ejercicio el reciproco ← . Sea I = (D, {R1, R2} , {})una interpretación arbitraria . Por el teorema 4.2.6 , vσI

(p(x) ∧ q(x)) =T para todas las asignaciones de todos los σI , y por la definición in-ductiva de la definición de una interpretación , vσI

(p(x)) = T y


vσI(q(x)) = T para toda asignación σI . Una vez más por el teore-

ma 4.2.6 , vI (∀xp(x)) = T y vI (∀xq(x)) = T , y por la definiciónde una interpretación vI (∀xp(x) ∧ ∀xq(x)) = T .

Mostrar que ∀ no se puede distribuir en la disyunción mediantela construcción de una interpretación falsa para ∀x (p (x) ∨ q(x)) ↔(∀x p (x) ∨ ∀x q(x)).

6. ∃x (p (x) ∨ q(x))↔ (∃x p (x) ∨ ∃x q(x))

7. ∀x (p (x)→ q(x))→ (∀x p (x)→ ∀x q(x))

Esta es una fórmula válida , pero su reciproca no lo es .

8. (∀x p (x)→ ∀x q(x))→ ∀x (p (x)→ q(x))

3.4. Equivalencias lógicas y substitución

3.4.1. Definición :Dadas dos fórmulas cerradas A1, A2 , si vI(A1) = vI(A2) para toda inter-pretación I , entonces A1 es logicamente equivalente a A2 . Notación: A1 ≡ A2 .

Sea A una fórmula cerrada y U un conjunto de fórmulas cerradas. Si para todas las interpretaciones I , vI(A) = T siempre que seavI(Ai) = T para toda Ai ∈ U , entonces A es una concecuencia lógicade U . Notación : U � A .


3.4.2. Lo que sigue es una tabla de fórmulas válidas encálculo de predicados

∀xA(x)↔ ¬∃x¬A(x) ∃xA(x)↔ ¬∀x¬A(x)∀x∀yA(x, y)↔ ∀y∀xA(x, y)∃x∀yA(x, y)→ ∀y∃xA(x, y)

∃x∃yA(x, y)↔ ∃y∃xA(x, y)

(∃xA(x) ∨B)↔ ∃x (A(x) ∨B) (∀xA(x) ∨B)↔ ∀x (A(x) ∨B)(B ∨ ∃xA(x))↔ ∃x (B ∨ A(x)) (B ∨ ∀xA(x))↔ ∀x (B ∨ A(x))(∃xA(x) ∧B)↔ ∃x (A(x) ∧B) (∀xA(x) ∧B)↔ ∀x (A(x) ∧B)(B ∧ ∃xA(x))↔ ∃x (B ∧ A(x)) (B ∧ ∀xA(x))↔ ∀x (B ∧ A(x))∀x (A→ B(x))↔ (A→ ∀xB(x)) ∀x (A(x)→ B)↔ (∃xA(x)→ B)

(∃x (A(x) ∨B(x)))↔ (∃xA(x) ∨ ∃xB(x)) (∀x (A(x) ∧B(x)))↔ (∀xA(x) ∨ ∀xB(x))(∀xA(x) ∨ ∀xB(x))→ ∀x (A(x) ∨B(x)) ∃x (A(x) ∨B(x))→ (∃xA(x) ∧ ∃xB(x))∀x (A(x)↔ B(x))→ (∀xA(x)↔ ∀xB(x)) ∀x (A(x)↔ B(x))→ (∃xA(x)↔ ∃xB(x))∃x (A(x)→ B(x))↔ (∀xA(x)→ ∃xB(x)) (∃xA(x)→ ∀xB(x))→ ∀x (A(x)→ B(x))∀x (A(x) ∨B(x))→ (∀xA(x) ∨ ∃xB(x)) ∀x (A(x)→ B(x))→ (∀xA(x)→ ∀xB(x))∀x (A(x)→ B(x))→ (∃xA(x)→ ∃xB(x)) ∀x (A(x)→ B(x))→ (∀xA(x)→ ∃xB(x))

3.4.3. Teorema :A ≡ B si y sólo si � A↔ B . U � A si y sólo si � (A1 ∧ · · · ∧An)→ A.

3.4.4. Observaciones :1. Si una subfórmula no contiene una variable libre entonces los cuantificado-

res de esa variable pueden ser pasados libremente a travez de la subfórmula, por ejemplo (∃xA(x) ∨B)↔ ∃x (A(x) ∨B).

2. Pasar cuantificadores a travez de implicaciones no es simple . Las fórmulasen la tabla pueden ser derivadas de fórmulas para disyunción y conjunción, mediante el reemplazo de la implicación por la disyunción equivalente yobservando la alternación de cuantificadores, tales como la negación , espasada a travez de ellos , aqui un ejemplo :

∃x (A(x)→ B(x)) ≡ ∃x (¬A(x) ∨B(x))

≡ ∃x¬A(x) ∨ ∃xB(x)

≡ ¬∃x¬A(x)→ ∃xB(x)

≡ ∀xA(x)→ ∃xB(x)


3.5. Lista de Ejercicios1. Simbolice en lógica de predicados la siguiente información de una sociedad

ficticia.

a) Nadie se puede casar con ningún primo de su cuñado.

b) Si alguien está soltero y su primo tiene una hija, tiene que casarsecon ella obligatoriamente.

c) Si alguien está soltera, y el cuñado de su tía tiene un hijo, tiene quecasarse con él.

d) Siempre hay alguien tal que si bebe, todo el mundo bebe.

e) Hay una persona tal que siempre que bebe, todo el mundo bebe.

f ) Si todo el mundo teme a Drácula y Drácula sólo me teme a mí,entonces yo soy Drácula.

g) O bien existen extraterrestres, o bien ningún ovni está tripulado, obien todos están tripulados por no extraterrestres.

2. En los argumentos siguientes: ¿Ud. A qué conclusión puede llegar?. De-muestre que su razonamiento es válido en lógica de predicados.

i

• Las mujeres divertidas no van al teatro.• Las profesoras de Matemáticas van al teatro.• Por lo tanto:◦ Algunas mujeres divertidas son profesoras de matemáticas.◦ Ninguna profesora de matemáticas es divertida.

ii

• Ningún idiota resulta entretenido.• Ningún premiado con el Nobel habla ininterrumpidamente.• Todos los que no resultan entretenidos hablan ininterrumpida-

mente.• Por lo tanto:◦ Algún idiota es premiado con el Nobel◦ Ningún idiota es premiado con el Nobel.

iii

• Algunos hombres son inteligentes.• Ninguna mujer miente.• Por lo tanto:◦ Algunos hombres que mienten son inteligentes.◦ Todas las mujeres que mienten son inteligentes.


iv

• Ningún individuo que siga estrictamente las leyes de la lógicatiene corazón.

• Todos los extraterrestres siguen estrictamente las leyes de la ló-gica.

• Por lo tanto:◦ Los extraterrestres carecen de corazón.◦ Existen extraterrestres que carecen de corazón.

3. Hallar una interpretación que haga falsa : ∃x p(x)→ p(a).

4. Determinar si las siguientes fórmulas son o no válidas :

a) ∃x (A(x)→ B(x))↔ (∀xA(x)→ ∃xB(x))

b) (∃xA(x)→ ∀xB(x))→ ∀x (A(x)→ B(x))

c) ∀x (A(x) ∨B(x))→ (∀xA(x) ∨ ∃xB(x))

d) ∀x (A(x) ∨B(x))→ (∃xA(x) ∨ ∃xB(x))

5. Simbolizar y demostrar , en lógica de predicados , la siguiente deducciónEduardo pudo haber visto al asesino.Antonio fue el primer testigo de la defensa.Eduardo estaba en clase o Antonio dio testimonio falso.Nadie en clase pudo haber visto al asesino.Por lo tanto : El primer testigo de la defensa dio testimonio falso

6. Simbolizar y demostrar en lógica de predicados la siguiente deducción

Lanzarote no ama a ninguno de sus amigos.

Lanzarote ama a la reina Ginebra.

Los amigos de Lanzarote odian aquellos a quienes Lanzarote ama.

El rey Arturo es Amigo de Lanzarote.

Por lo tanto : Arturo odia a Ginebra

7. Sea un universo de discurso que consta de tres personas solamente , asaber , Juan ,María , y Juana . Los tres son estudiantes , y ninguno deellos es rico . Juan es hombre mientras que María y Juana son mujeres . S, F , M , y R denotan respectivamente las propiedades estudiante ,mujer, hombre , y rico .

a) Presentar la asignación de los predicados S , F , M , y R.

b) Interpretar las siguientes expresiones :∀xS(x) , ∀xF (x) ∨ ∀xM(x) , ∀x (F (x) ∨M(x)) , ∃x (F (x)→ R(x))

8. En las siguientes expresiones, determine un modelo y un contraejemplo


a) Nadie sino los valientes merecen a Ginebra.

b) En toda pareja de vecinos hay algún envidioso.

9. Sea F (t1) = t1 encuentra el error y seaQ = error del programapuede ser corregido. Traduzca la expresión ∀xF (x)→ Q a una oración en español.

10. Realizar un análisis semántico de la fórmula :∃x∀y ((p (x, y) ∧ ¬p (y, x))→ (p (x, x)↔ p (y, y)))

Bibliografía

[1] Ben-Ari Mordechai. Mathematical Logic for Computer Science. Springer-Verlag (Second Edition), Great Britain, 2004.

[2] Pascual Julián Iranzo, María Alpuente Frasnedo. Programación Lógica: de-puración, verificación, certificación. Pearson, Madrid, 2007.

[3] Teresa Hortalá González, Narciso Martí Oliet, Miguel Palomino Tarjuelo,Mario Rodríguez, Rafael del Vado Vírseda. Lógica Matemática para Infor-máticos. Pearson, Madrid, 2008.

[4] Pascual Julián Iranzo. Lógica Simbólica para Informáticos. Alfaomega - Ra-Ma, México 2005.

[5] Enrique Paniagua Arís, Juan Luis Sánchez González, Fernando Martín Ru-bio. Lógica Computacional. Thomson, España 2003.

[6] Pedro Cabalar. Lógica Computacional. Departamento de Computación Uni-versidad de la Coruña, España, 2008

[7] Miguel Palomino Tarjuelo. Reflexión, abstracción y simulación en la “ lógicade reescritura “. Departamento de Sistemas Informáticos y Programaciónde la Facultad de Ciencias Matemáticas de la Universidad Complutense deMadrid Noviembre 2004.

102

Libro.logicaComputacional

Documents

Transcript of Libro.logicaComputacional