En la clase de hoy del curso Lógica matemática y fundamentos se ha explicado cómo formalizar en lógica proposicional los argumentos de los ejercicios 8 y 9 de la relación 4 y cómo demostrar con Isabelle/HOL su corrección.
Los ejercicios y sus soluciones se muestran a continuación:
Read More “LMF2013: Ejercicios de argumentación en lógica proposicional con Isabelle/HOL”
En la clase de hoy del curso Lógica matemática y fundamentos se comentado distintas cuestiones.
En primer lugar, se ha respondido la pregunta de cómo demostrar por deducción natural la fórmula (¬q → ¬p) ∨ (q → p). Su dificulad está en el uso del principio del tercio excluso y en la demostración por casos (eliminación de la disyunción).
En segundo lugar, se ha respondido la pregunta de cómo usar lemas auxiliares en las demostraciones con Isabelle/HOL.
En tercer lugar, se ha comentado que APLI2 sólo comprueba que la formalización es correcta; pero no que el argumento sea correcto.
En cuarto lugar, se ha explicado cómo se puede demostrar automáticamente argumentos que no se puede con el método auto, pero sí con metis o meson. Como ejemplo, se ha demostrado el ejercicio 8 de la relación 6 con metis.
En quinto lugar, se ha explicado cómo se puede comprobar que los modelos calculados por QuickCheck son contramodelos. Para ello, se ha usado el ejercicio el ejercicio 13 de la relación 6.
Para resaltar la importancia del principio del tercio excluso, se ha demostrado que:
Finalmente, terminamos comentando cuestiones de filosofía de la matemática. En particular, sobre el formalismo, el intuicionismo y el constructivismo.
En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos estudiado el tipo abstracto de los polinomios y su implementación en Haskell.
Comenzamos la clase analizando las posibles representaciones de los polinomios y, como consecuencia, establecer la signatura y las propiedades del TAD de los polinomios.
A continuación, estudiamos tres prosibles representaciones del TAD de los polinomios: mediante tipos algebraicos, mediantes listas dispersas y mediante listas densas.
Finalmente, estudiamos la implementación de los polinomios como tipo algebraico y mediantes listas dispersas.
Las transparencias usadas en la clase son las páginas 1-29 del tema 21
Read More “I1M2012: El TAD de los polinomios en Haskell (1)”
En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha comentado el 4º examen de la evaluación continua.
Se ha resaltado los puntos de mayor dificultad:
A continuación se muestra el examen junto con su solución:
Read More “I1M2012: Comentario del 4º examen de la evaluacion continua”
En las clases del miércoles y de hoy del curso Lógica matemática y fundamentos se ha continuado comentando soluciones de los ejercicios de deducción natural en lógica proposicional con Isabelle/HOL de la relación 3.
También se han comentado ejercicios de la relación 4 (de argumentación proposicional con Isabelle/HOL) y de la relación 5 (de eliminación de conectivas).
Se ha propuesto la solución de los ejercicios de la relación 6 (sobre formalización de argumentos en lógica de primer orden).
Finalmente, se ha propuesto como tarea el enviar por correo la solución mediante deducción natural de 3 ejercicios elegidos entre los propuestos en los exámenes de los temas 2, 3 y 5 del libro de ejercicios.