DeduccionNatural.pl: herramienta escrita en Prolog para el aprendizaje de la asignatura de Lógica

Abstract

La lógica matemática y computacional son materias básicas en la mayoría de las titulaciones universitarias relacionadas con la Ingeniería Informática, tanto en España como en el extranjero. Son fundamentales en el estudio de bases de datos, complejidad computacional, lenguajes de programación, inteligencia artificial, diseño y verificación de sistemas hard y soft, entre otros. Sin embargo, para estudiantes de un primer curso no es inmediato reconocer las conexiones entre la lógica y lo que necesitarán aprender en estudios futuros. Para mitigar esta sensación de desconexión entre contenidos básicos y más avanzados, hemos desarrollado DeduccionNatural.pl, un programa con licencia de código abierto escrito en Ciao Prolog (lenguaje de programación lógico), que permite comprobar si una demostración de deducción natural (en lógica proposicional) es correcta. En DeduccionNatural.pl, las demostraciones son programas, las reglas de inferencia son funciones de una librería predefinida, y las reglas derivadas sonsubrutinas (para refactorizar las demostraciones) definidas por los estudiantes. Durante el curso 2021–2022 hemos utilizado DeduccionNatural.pl en los grados de Ingeniería de Ciberseguridad y de Inteligencia Artificial en la Universidad Rey Juan Carlos y hemos realizado una encuesta de satisfacción. Los resultados no son concluyentes, pero nos animan a seguir mejorando la herramienta.

Mathematical and computational logic are basic subjects in most university degrees related to Computer Engineering, both in Spain and abroad. They are fundamental in the study (among other topics) of databases, computational complexity, programming languages, artificial intelligence, design and verification of hard and soft systems. However, for first-year un-dergraduate students it is not immediate to recognize the connections between logic and what they will need to learn in future studies. To mitigate this feeling of disconnect between basic and more advanced content, we have developed DeduccionNatural.pl, an open source licensed program written in Ciao Prolog (a Logic Programming Language), which allows to check if a natural deduction proof (in propositional logic) is correct. In DeduccionNatural.pl, the proofs are programs, the inference rules are functions of a predefined library, and the derived rules are subroutines (to refactor the proofs) defined by the students. During the academic year 2021-2022, we have used DeduccionNatural.pl in the Cybersecurity Engineering and Artificial Intelligence degrees at Universidad Rey Juan Carlos and we have conducted a satisfaction survey. The results are not conclusive, but they encourage us to continue improving the tool.