Proof assistant based on didactic considerations

PorJosé A. Alonso

Se ha publicado un artículo sobre el uso de sistemas de razonamiento en la enseñanza de la lógica titulado Proof assistant based on didactic considerations.

Sus autores son Jorge Pais y Álvaro Tasistro (de la Universidad ORT Uruguay, Uruguay).

Su resumen es

We consider some issues concerning the role of Formal Logic in Software Engineering education, which lead us to promote the learning of formal proof through extensive, appropriately guided practice. To this end, we propose to adopt Natural Deduction as proof system and to make use of an adequate proof assistant to carry out formal proof on machine. We discuss some necessary characteristics of such proof assistant and subsequently present the design and implementation of our own version of it. This incorporates several novel features, such as the display and edition of derivations as trees, the use of meta-theorems (derived rules) as lemmas, and the possibility of maintaining a set of draft trees that can be inserted into the main derivation as needed. The assistant checks the validity of each edition operation as performed. So far, it has been implemented for propositional logic and (quite satisfactorily) put into practice in courses of Logic for Software Engineering and Information Systems programs.

El artículo se ha publicado en Journal of Universal Computer Science.

La Lógica en las ciencias computacionales

PorJosé A. Alonso

Se ha publicado un artículo sobre la enseñanza de la lógica titulado La Lógica en las ciencias computacionales.

Su autor es Edgar Serna M. (del Instituto Tecnológico Metropolitano, Medellín (Colombia)).

Su resumen es

En este trabajo se hace un análisis a la necesidad de incluir a la lógica en los procesos formativos en Ciencias Computacionales (CS por sus siglas en inglés). Se parte de un recorrido sobre la historia de la lógica en estas ciencias, posteriormente se describe la relación y la necesidad de incluirla en los procesos formativos relacionados, y al final se analiza qué, cuándo y qué tan profundo se debería trabajar en la formación en CS. Se trata de una revisión al estado del tema y a la importancia de incluirlo en los pregrados y en los posgrados en áreas de ciencias computacionales y tecnologías de información.

El artículo se ha publicado en la Revista Educación en Ingeniería.

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.

Determinación, esperanza y éxitos en la resolución de problemas

PorJosé A. Alonso

Uno de mis libros favoritos es Cómo plantear y resolver problemas de G. Pólya. Suelo releerlo periódicamente y en la lectura de hoy me ha llamado la atención el siguiente párrafo sobre la importancia de las emociones en la resolución de problemas

Sería un error el creer que la solución de un problema es un “asunto puramente intelectual”: la determinación, las emociones, juegan un papel importante. Una determinación un tanto tibia, un vago deseo de hacer lo menos posible pueden bastar a un problema de rutina que se plantea en la clase; pero, para resolver un problema científico serio, hace falta una fuerza de voluntad capaz de resistir durante años de trabajo amargos fracasos.

y sus consecuencias en la enseñanza

Cuando un alumno comete errores verdaderamente garrafales, cuando es de una lentitud exasperante, casi siempre es por las mismas razones; no tiene absolutamente ningún deseo de resolver el problema, no desea incluso comprenderlo como es debido, y por tanto, no lo comprende. Así, el profesor que desee realmente ayudar a un alumno, debe ante todo despertar su curiosidad, comunicarle el deseo de lograrlo. Debe también conceder al alumno un cierto tiempo para reflexionar, al cabo del cual quizá se decida a trabajar.