En la clase de hoy del curso Lógica matemática y fundamentos se han resuelto los ejercicios 22, 27, 28, 29, 32 y 34 de la relación 7 sobre deducción natural en lógica de primer orden con Isabelle/HOL.
Las soluciones de los ejercicios resueltos se muestran a continuación:
Read More “LMF2013: Ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL (2)”
En la clase de hoy del curso Lógica matemática y fundamentos se han resuelto los ejercicios 10, 11, 12, 13 y 16 de la relación 7 sobre deducción natural en lógica de primer orden con Isabelle/HOL.
Las soluciones de los ejercicios resueltos se muestran a continuación:
Read More “LMF2013: Ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL (1)”
En la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado la deducción natural en la lógica de primer orden.
Las transparencias de estas clases son las del tema 8.
A la vez que se presentaba las reglas, se ha comentado su formalización en Isabelle/HOL. La teoría correspondiente es
Read More “LMF2013: Deducción natural en lógica de primer orden”
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.