LI2014: Deducción natural proposicional (1)

En la la clase de hoy del curso de Lógica Informática se ha empezado el estudio de la deducción natural proposicional.

Terminado el estudio semántico (cuyo problema fundamental es dado un conjunto de fórmulas S y una fórmula F, decidir si F es consecuencia de S (en notación, S |= F)), comenzamos el estudio de los cálculos deductivos (cuyo problema fundamental es dado un conjunto de fórmulas S y una fórmula F, decidir si F es deducible de S (en notación, S |- F)). Además, se requiere que los cálculos sean adecuados y completos (es decir; que S |= F si, y sólo si, S |- F).

El primer cálculo deductivo que estudiamos es el de deducción natural. Las reglas que se han visto en la clase de hoy son las de la conjunción, de la doble negación, de eliminación del condicional, de modus tollens, de introducción del condicional y las de la disyunción.

Finalmente, se ha mostrado cómo editar demostraciones usando el sistema Pandora. Los ejemplos vistos en clase se encuentran en los vídeos del ejemplo 1 y ejemplo 2.

Las transparencias de esta clase son las páginas 1-12 del tema 2
Read More “LI2014: Deducción natural proposicional (1)”

LI2014: Semántica de la lógica proposicional (2)

En la primera parte de la clase de hoy del curso de Lógica Informática se ha demostrado la equivalencia de los siguientes problemas

  1. decidir si una fórmula es consecuencia lógica de un conjunto finito de fórmulas,
  2. decidir si una fórmula es una tautología,
  3. decidir si una fórmula es insatisfacible y
  4. decidir si un conjunto de fórmulas es inconsistente.

Como aplicación se ha visto la decisión de la corrección de un argumento y la resolución de rompecabezas lógicos.

También, se ha explicado cómo se puede usar en la resolución de los anteriores problemas el Gateway to Logic.

En la segunda parte de la clase se han comentado las soluciones de los ejercicios de la 1ª relación y se han propuesto los de la 2ª relación.

Las transparencias de esta clase son las páginas 31-34 del tema 1
Read More “LI2014: Semántica de la lógica proposicional (2)”

I1M2014: Definición de funciones elementales en Haskell

En la segunda parte de la clase de hoy del curso Informática (de 1º de Grado en Matemáticas) se ha estudiado cómo definir funciones en Haskell usando los formas básicas: composición, condicionales, guardas y patrones.

También se ha explicado cómo comprobar con QuickCheck propiedades de programas. Como ejemplo, se han comentado la comprobación de la equivalencia de las distintas definicones propuestas en la 1ª relación de ejercicios.

Como tarea para la próxima clase se ha propuesto resolver de manera colaborativa los ejercicios de la 2ª relación.

Las transparencias usadas en la clase son las del tema 4.
Read More “I1M2014: Definición de funciones elementales en Haskell”

I1M2014: Tipos y clases en Haskell

En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado los tipos y las clases en Haskell. Los objetivos de tema son aprender

  • qué es un tipo,
  • cómo expresar que una expresión tiene un tipo determinado,
  • cómo preguntar a Haskell por el tipo de una expresión,
  • cómo determinar el tipo de una expresión,
  • cuáles son los tipos básicos (Bool, Char, String, Int, Integer, Float y ,
  • cuáles son los tipos compuestos (listas, tuplas y funciones),
  • qué es el polimorfismo y la sobrecarga de funciones y
  • cuáles son las clases básicas (Eq, Ord, Show, Read, Num, Integral y Fractional), sus métodos e instancias.

Las transparencias usadas en la clase son las del tema 3:
Read More “I1M2014: Tipos y clases en Haskell”