LI2011-12: Aplicaciones de la lógica proposicional con Prover9 y Mace4

PorJosé A. Alonso

En la clase de hoy del curso Lógica Informática hemos visto cómo resolver lógicamente problemas representándolos en la lógica proposicional y usando Prover9/Mace4 para su solución.

Los problemas que se han visto son

  • El problema de los veraces y los mentirosos.
  • El problema de los animales.
  • El problema del coloreado del pentágono.
  • El problema del palomar.
  • El problema de los rectángulos.
  • El problema de las 4 reinas.
  • El problema de Ramsey.

Como tarea pendiente se propone la solución de problemas análogos siguiendo la misma estructura que los anteriores:

  1. Enunciado.
  2. Simbolización.
  3. Representación.
  4. Búsqueda de la prueba (con Prover9) o de modelos (con Mace4).
  5. Conclusión.

Las transparencias utilizadas son las del tema 5b
Read More “LI2011-12: Aplicaciones de la lógica proposicional con Prover9 y Mace4”

Libro de ejercicios resueltos de programación en Haskell (versión del 9 de Noviembre de 2011)

PorJosé A. Alonso

A lo largo del curso iré actualizando un libro de ejercicios resueltos de programación con Haskell con las relaciones de ejercicios del curso de Informática (de 1º del Grado en Matemáticas)

En la versión actual contiene las soluciones de las 6 primeras relaciones que tratan sobre definiciones elementales, definiciones por comprensión y definiciones por recursión.

I1M2011: Ejercicios de definiciones por recursión en Haskell (2)

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos continuado los comentarios sobre las soluciones de los ejercicios de la 6ª relación, que tratan sobre definiciones por recursión, que comenzamos en la clase anterior.

Los ejercicios, y sus soluciones, se muestran a continuación:
Read More “I1M2011: Ejercicios de definiciones por recursión en Haskell (2)”

Reseña: Philosophy of mathematics and computer science

PorJosé A. Alonso

Kazimierz Trzęsicki (del Departamento de Lógica, Informática y Filosofía de la Ciencia de la Universidad de Białystok, Polonia) ha publicado el artículo Philosophy of mathematics and computer science.

El resumen del artículo es

It is well known fact that the foundation of modern computer science were laid by logicians. Logic is at the heart of computing. The development of contemporary logic and the problems of the foundations of mathematics were in close mutual interaction. We may ask why the concepts and theories developed out of philosophical motives before computers were even invented, prove so useful in the practice of computing. Three main programmes together with the constructivist approach are discussed and the impact on computer science is considered.

En el artículo comenta las aportaciones a la ciencia de la computación de las tres escuelas lógicas de los fundamentos de la matemática:

  • del logicismo (de Frege, Russell y Withehead) resalta el sintaxis de la lógica como primer lenguaje de programación, los tipos, el lamda cálculo, LISP, la programación funcional y la lógica combinatoria como lenguaje de programación.
  • del formalismo (de Hilbert) destaca la máquina de Turing (como medio para resolver los problemas de decibilidad), la teoría de la computación, la demostración automática y el razonamiento formalizado.
  • del intuicionismo (de Brouwer) y del constructivismo (de Markov y Bishop) destaca la visión de “fórmulas-como-tipos”, la extracción de programas a partir de las pruebas, la teoría costructiva de tipos de Martin-Löf, los sistema de demostración asistida (Automath, NuPRL, LEGO, Agda, Twelf y Coq) y las teorías desarrolladas con dichos sistemas.