Reseña: “An intelligent tutoring system for teaching FOL equivalence”

PorJosé A. Alonso

Se ha publicado un artículo sobre enseñanza de la lógica titulado An intelligent tutoring system for teaching FOL equivalence.

Sus autores son Foteini Grivokostopoulou, Isidoros Perikos, Ioannis Hatzilygeroudis (de la Universidad de patras en Grecia).

El trabajo se ha presentado hoy en el AIEDCS 2013 (The First Workshop on AI-supported Education for Computer Science).

Su resumen es

In this paper, we present an intelligent tutoring system developed to assist students in learning logic. The system helps students to learn how to construct equivalent formulas in first order logic (FOL), a basic knowledge representation language. Manipulating logic formulas is a cognitively complex and error prone task for the students to deeply understand. The system assists stu- dents to learn to manipulate and create logically equivalent formulas in a step-based process. During the process the system provides guidance and feedback of various types in an intelligent way based on user’s behavior. Evaluation of the system has shown quite satisfactory results as far as its usability and learning capabilities are concerned.

LMF2013: Ejercicios de argumentación en lógica proposicional con Isabelle/HOL

PorJosé A. Alonso

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”

LMF2013: Misceláneas

PorJosé A. Alonso

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:

  • la fórmula ∃x(P(x) → ∀yP(y)) es correcta y
  • existen dos números irracionales x e y tales que xʸ es racional.

Finalmente, terminamos comentando cuestiones de filosofía de la matemática. En particular, sobre el formalismo, el intuicionismo y el constructivismo.

LMF2012: Tableros semánticos en Haskell

PorJosé A. Alonso

En la clase de hoy del curso de Lógica matemática y fundamentos (de 3º de Grado en Matemáticas) se ha comentado las soluciones de los ejercicios sobre la implementación en Haskell de los tableros semánticos.

Las soluciones de los ejercicios se muestran a continuación. En los ejercicios se usa el módulo SintaxisSemantica desarrollado en la clase del día 13 de marzo.
Read More “LMF2012: Tableros semánticos en Haskell”