ADN : una herramienta para la enseñanza de la Deducción Natural Faraón Llorens, Sergio Mira Dpto. Ciencia de la Computación e Inteligencia Artificial Escuela Politécnica Superior Universidad de Alicante [email protected]

Resumen Se presenta el Asistente para la Deducción Natural (ADN), aplicación diseñada y desarrollada en el departamento de Ciencia de la Computación e Inteligencia Artificial de la Universidad de Alicante, con el objetivo de servir de ayuda, tanto al profesor como a los estudiantes, en la enseñanza de las técnicas de demostración matemática, en concreto de la Deducción Natural. Esta herramienta didáctica se está utilizando en las asignaturas “Lógica de Primer Orden” de primer curso de la licenciatura en Matemáticas y “Lógica Computacional” de primer curso de las ingenierías en Informática (tanto las dos técnicas como la superior). ADN (Asistente para la Deducción Natural) es un programa, ejecutado vía web, que supervisa y comprueba que las fórmulas lógicas introducidas están sintácticamente bien construidas (fbf) y que la secuencia obtenida (pasos de la deducción) es correcta. Al mismo tiempo contiene un breve tutorial sobre la Deducción Natural. También dispone de otras herramientas de soporte: árbol sintáctico, aconsejador, ayuda en línea, información detallada de errores, entre otros. 1. Introducción Un profesor, de cualquier nivel educativo, debe enfrentarse a la tarea de trasmitir conocimiento. Y no siempre saber de un tema lleva asociado el saber comunicarlo. Los distintos niveles educativos no han puesto el mismo énfasis en preparar a los profesores en los aspectos didácticos. Los niveles iniciales se preocupan más en cómo se enseña que en qué se enseña, mientras que los niveles superiores, tradicionalmente, se centran más en qué se enseña, y el estudiante ya se preocupará de aprender. Afortunadamente

está tendencia está cambiando, y en la Universidad cada vez es mayor el numero de profesores que se interesan por los aspectos didácticos de sus materias. Pero aún queda mucho por hacer, y en la universidad española la docencia está en clara inferioridad con respecto a la investigación. No existe una fórmula única, mágica y universal. Cada campo, área, materia e incluso tema puede necesitar de un enfoque distinto. Cada profesor debe diseñar su estrategia para enseñar (y complementariamente que el estudiante aprenda) su asignatura. La nuevas tecnologías pueden ayudarnos a ello. El uso de los ordenadores no es un beneficio en sí mismo, pero si que podemos aprovechar sus características para sacar ventajas en nuestra tarea. La aplicación aquí presentada surge de la tarea de impartir asignaturas relacionadas con la lógica en primer curso del nivel universitario, de la preocupación y el respeto por la tarea docente y el interés por las nuevas tecnología de la información y las comunicaciones. Todo ello conjugado, hace que observando las dificultades que tienen los estudiantes para aprender la técnica de la deducción natural y los errores que cometen, hayamos diseñado una herramienta didáctica que ejecutada en un ordenador, evite que el estudiante cometa esos errores y la ayude en los aspectos más dificultosos. Aunque la aplicación ADN únicamente puede servir a los profesores que tengan que enseñar la técnica de la deducción natural, la reflexión puede ser exportable. 2. Lógica ¿Qué es conocimiento? podríamos decir que es el hecho o la condición de conocer algo que hemos adquirido por experiencia o asociación. Los seres humanos vamos adquiriendo conocimiento al ver, oír, tocar, sentir y oler el mundo que nos rodea. Y ese conocimiento lo almacenamos en nuestro cerebro. Se han desarrollado distintos formalismos para representar y manipular el conocimiento humano. En el enfoque simbólico se utilizan símbolos para representar el conocimiento y el estado del mundo y se simula el proceso cognitivo mediante manipulación de esos símbolos. La Lógica de Predicados pone a nuestra disposición un lenguaje que nos permitirá formalizar expresiones del conocimiento humano haciendo explícitos los objetos y las relaciones, así como sus restricciones. Además nos proporciona un método, la deducción matemática, para obtener nuevo conocimiento a partir del antiguo. Es por ello que la lógica se convierte en una asignatura presente en los primeros cursos

de distintas titulaciones, ya que proporciona una base formal de trabajo [Reeves1990, Garrido1995, Llorens1996]. En la actualidad existe un variado número de herramientas que pueden servir de ayuda en el aprendizaje de la lógica [Goldson1993, Barwise2000, TTL2000]. a. Lenguaje La lógica pretende formalizar las expresiones del conocimiento humano. Y dicho conocimiento lo adquirimos y transmitimos por medio del lenguaje. Pero el lenguaje natural que utilizamos es ambiguo y engorroso, y por ello, para trabajar formalmente con el conocimiento, necesitamos un lenguaje artificial. En la definición de ese lenguaje formal empezaremos por determinar el alfabeto (conjunto de símbolos) que utilizaremos y las frases (fórmulas bien formadas) que podremos construir con combinaciones autorizadas de sus símbolos. Así, ante una sentencia del lenguaje natural buscaremos sus componentes : •

Qué se afirma, es decir, las propiedades y relaciones que aparecen en la sentencia y que representaremos en forma de predicados.

•

De quienes se afirma, es decir, los objetos o individuos a los que hace referencia la sentencia y que representaremos por medio de términos.

Cuando los predicados se aplican a un solo término se trata de propiedades o características de dicho objeto; cuando hacen referencia a varios sujetos suelen representar relaciones. Los objetos deben pertenecer a un dominio genérico o universo del discurso, y pueden ser : •

Constantes: representan objetos concretos del dominio.

•

Variables: permiten referenciar cualquier elemento del universo.

•

Funciones: denotan objetos referenciados en función de otros objetos.

Así, con un predicado y los términos implicados en dicho predicado podemos formar fórmulas atómicas o elementales. Combinando dichas fórmulas atómicas mediante las conectivas lógicas (conjunción "∧", disyunción "∨", negación "¬" e implicación "→") obtendremos fórmulas moleculares. Por último, si queremos expresar la cantidad de objetos que satisfacen alguna condición utilizaremos los cuantificadores, el universal "∀" (todos los elementos del universo del discurso) y el existencial "∃" (por lo menos un individuo del universo).

En el apartado de la lógica como lenguaje representación de conocimiento, las principales dificultades que hemos detectado en los estudiantes son en relación a tres aspectos: •

Traducción de sentencias de lenguaje natural en fórmulas lógica.

•

Estructura lógica de las fórmulas.

•

Alcance de los cuantificadores.

Al diseñar el asistente hemos tenido en cuenta estos aspectos y de qué forma podemos ayudar a nuestros estudiantes. ADN utiliza el alfabeto clásico de la Lógica de Primer Orden y la definición usual de fórmula bien formada (fbf). En aras a obtener una representación más clara el asistente impone dos restricciones para la construcción de las fórmulas: 1. No permite introducir fórmulas con variables libres. 2. Las conectivas →, ∧ y ∨ son operaciones binarias, y por ello deben estar agrupadas de dos en dos. Así, P∧Q∧R sería incorrecto; la forma de introducirla sería (P∧Q)∧R o cualquier otra combinación con paréntesis. ADN va realizando un análisis sintáctico de la fórmula a medida que la vamos introduciendo, de forma que no permite introducir símbolos que no pertenezcan al alfabeto. Además va coloreando cada variable de forma que se distingue claramente a qué variables afecta cada cuantificador, ya que cada variable se identifica por su nombre y color. Por otro lado, la representación de las fórmulas en forma de árbol etiquetado nos puede ayudar a ver claramente la estructura sintáctica de las mismas. El árbol sintáctico de la fórmula bien formada P(a) → ∃y P(y), proporcionado por el programa ADN, lo podemos ver en la Figura 1. El árbol sintáctico de una fórmula lógica nos permite distinguir claramente cuál es el operador principal y las prioridades entre ellos. Esto nos ayudará en la comprensión del significado de la fórmula y en la posterior manipulación sintáctica cuando tengamos que aplicar las reglas de la deducción.

Figura 1: Árbol sintáctico

b. Deducción Natural El razonamiento es el proceso cognitivo por medio del cual utilizamos y aplicamos nuestro conocimiento, permitiéndonos pasar de una información a otra relacionada con esta. Sin la posibilidad de hacer inferencias, el sistema de procesamiento de información se vería obligado a tener que definir todas las situaciones puntuales y específicas con las que se debe enfrentar. A las sentencias de las cuales partimos en el proceso de razonamiento se les llama premisas y a la sentencia a la cual llegamos se le denomina conclusión. Las premisas junto a la conclusión forman el argumento. El concepto lógico de deducción correcta dice que de premisas verdaderas debemos obtener conclusión verdadera, es decir, no podemos aceptar que las premisas sean verdaderas y la conclusión falsa. La lógica nos proporciona métodos de cálculo que nos permiten inferir, por simple manipulación sintáctica, nuevas fórmulas a partir de las conocidas [Socher-Ambrosius1997].

Uno

de

estos

métodos

es

la

Deducción

Natural

[Gentzen1934], cuyo mecanismo está muy cercano al razonamiento intuitivo del ser humano. Así, de forma sencilla, a partir de las fórmulas dadas como premisas y con el único apoyo de unas reglas básicas, obtenemos determinadas conclusiones. La idea básica es la de desmenuzar el salto cognitivo que va de las premisas a la conclusión en pequeños pasos que hemos acordado como correctos. Así, si asumimos

las premisas y cada paso elemental que damos lo justificamos con una regla básica, iremos obteniendo nuevas fórmulas lógicas que podemos asumir como conclusiones derivadas de las premisas. Todas las fórmulas lógicas que vamos introduciendo, una vez comprobada su corrección (son fórmulas bien formadas) y su validez (se derivan de acuerdo a las reglas dadas) son visualizadas en la parte central de la ventana del ADN, que llamaremos pizarra. b1) Reglas básicas Para determinar las reglas básicas de la Deducción Natural nos basaremos en la idea de montar y desmontar fórmulas lógicas, de forma que desmontando las premisas en sus componentes básicas (fórmulas atómicas) podamos montar la conclusión a partir de ellas. Así dispondremos de dos reglas (una de introducción y otra de eliminación) para cada símbolo lógico (conectivas y cuantificadores). Si la regla básica introduce en su conclusión una conectiva o cuantificador que no aparece en sus premisas será una regla de introducción; si elimina de su conclusión una conectiva o cuantificador que aparece en sus premisas será una regla de eliminación. Se intuye que si disponemos de procedimientos para añadir o quitar los distintos símbolos lógicos, podremos transformar por pura manipulación sintáctica las premisas en la conclusión. Desde un punto de vista de ingeniería, se trataría de desmontar las fórmulas lógicas que tenemos como premisas hasta obtener sus componentes básicas (fórmulas atómicas) y volver a montarlas en la configuración adecuada (fórmula lógica que queremos obtener como conclusión). Las reglas serían los instrumentos que nos permitirían montar y desmontar dichas fórmulas lógicas. Tendremos un deducción correcta cuando consigamos una secuencia finita de fórmulas, donde cada una de las fórmulas ha sido obtenida mediante la aplicación de alguna regla de inferencia. Las fórmulas iniciales de esa secuencia serán las premisa de las que partimos y la última fórmula obtenida la conclusión. En ADN, cada línea de nuestra deducción (y por tanto la fórmula lógica escrita en ella) estará "justificada" por la aplicación de una regla básica a alguna o algunas líneas anteriores. Dicha justificación aparece en la columna de la derecha. Por ejemplo, en la figura del ejemplo del final, la justificación de la línea 10 que dice ED 1,2-5,6-9 significa que esa fórmula la hemos obtenido porque tenemos en la línea 1 una fórmula cuya conectiva

principal es una disyunción; suponemos en la línea 2 una de las dos alternativas y obtenemos cierta conclusión condicionada en la línea 5; suponemos en la línea 6 la otra alternativa y obtenemos la misma conclusión condicionada en la línea 9; y llegamos en la línea 10 a que dicha conclusión ya no esta condicionada, porque queda justificada por la regla de Eliminación del Disyuntor o Prueba por Casos. b2) Subdeducciones Otro de los aspectos cruciales de la deducción natural es el de las subpruebas (subdeducciones o subderivaciones). En cualquier paso de nuestra deducción podemos introducir un supuesto provisional, que debe ser cancelado en alguna línea posterior. Desde el supuesto hasta la cancelación tendremos una subdeducción. Así, en nuestras deducciones tendremos fórmulas a distintos niveles, que visualizaremos gráficamente mediante una sangría a la derecha. Los supuestos provisionales son una herramienta muy potente ya que nos permiten suponer lo que nosotros queramos. Pero debemos pagar un alto precio por ello: para poder finalizar una demostración deberemos haber cancelado todos los supuestos que hayamos hecho. Por tanto, la cancelación de supuestos provisionales se convierte en una pieza clave de las deducciones naturales. Cuando un supuesto es cancelado, sangramos a la izquierda y sombreamos en gris las fórmulas interiores de la subdeducción. Dichas fórmulas interiores serán inaccesibles a partir de este momento. La utilización de subdeducciones nos permite "modularizar" nuestras deducciones, planteándonos subobjetivos más sencillos que el objetivo final, y que en su conjunto nos lleven a la conclusión que buscamos. Una vez realizada una subdeducción esta podría considerarse como una regla derivada y utilizarse a partir de ese momento. Estas reglas derivadas permiten ir incrementando nuestro sistema de reglas. En la técnica de la deducción natural, las principales dificultades que hemos detectado en los estudiantes son en relación a cuatro aspectos: •

Saltos cognitivos que no justifican (bien porque los consideran evidentes o bien porque no saben cómo hacerlo).

•

Aplicación incorrecta de las reglas.

•

Manejo incorrecto de las subdeducciones (tanto en la cancelación como en la utilización de líneas interiores de una subdeducción una vez cancelada).

•

Quedarse parados y no saber por donde continuar.

Al diseñar el asistente hemos tenido en cuenta estos problemas de forma que esta herramienta pueda ayudar a nuestros estudiantes. Algunas de las ventajas que ofrece el ADN para realizar deducciones ya han sido comentados al explicar la técnica de la deducción natural y otros serán comentados en el siguiente apartado. 3. Asistente para la Deducción Natural (ADN) Vamos a presentar una herramienta didáctica de apoyo para el aprendizaje de la técnica de Deducción Natural. Dicha herramienta ha sido diseñada y desarrollada en el departamento de Ciencia de la Computación e Inteligencia Artificial de la Universidad de Alicante. Esta herramienta pretende ser un instrumento didáctico que ayude a los estudiantes a escribir fórmulas lógicas bien formadas y a realizar deducciones correctamente. No se trata de un sistema que construya demostraciones de forma automática; simplemente es un asistente que supervisará y guiará al estudiante en el proceso, ayudándola a elaborar sus propias deducciones. Comprueba si la fórmula es sintácticamente correcta (fbf) y si se ha obtenido de forma adecuada (aplicación de las reglas básicas). Además, posee algunas herramientas de apoyo, como el visor de árboles sintácticos de las fórmulas, informe detallado de los errores, visor de reglas básicas, aconsejador y ayuda en línea. ADN ([Llorens2000]) puede ser ejecutado con cualquier navegador, ya que se trata de un applet escrito en Java. Se encuentra disponible en internet en el sitio web: http://www.dccia.ua.es/logica/ADN La aplicación se ejecuta vía internet, para ello el ordenador debe estar concetado a la red. También se dispone de una versión para instalación en el ordenador y ejecutarlo de manera local, sin necesidad de conexión a la red. De cualquier modo, al jecutarlo se bre una ventana de la Figura 2. Desde aquí podemos acceder a los dos partes de la aplicación: el tutorial de deducción natural y la aplicación que permite realizar deducciones.

Figura 2: Ventana principal

a. Tutorial La aplicación desarrollada va acompañada de una concisa, pero clara, descripción de la técnica de la deducción natural, así como de la forma en que debemos realizar las deducciones con el ADN. También se han incluido una serie de ejemplos ya resueltos y ejercicios para resolver. Se acompaña también de una extensa documentación (en pdf), con manual de usuario y los distintos artículos y documentos que se van generando. En la Figura 3 podemos ver la ventana del tutorial, con el índice de los distintos apartados. Finalmente, destacar por su carácter didáctico las animaciones de deducciones que podemos encontrar en el tutorial (en el apartado de los ejemplos). La animación de la Figura 4, realizada en flash, representa por sí sola un ejemplo claro de la utilización de los recursos multimedia como mejora de nuestra tarea docente (evidentemente en el papel no podemos valorar su utilidad).

Figura 3: Ventana tutorial

Figura 4: Animación

b. Aplicación En la Figura 5 se muestra la pantalla principal del ADN y las partes en las que se divide la misma: 1. Editor de la fórmula objetivo: nos permite editar la fórmula que será el objetivo de la deducción. 2. Cuerpo de la deducción (pizarra): en esta zona se irán visualizando los pasos de la deducción. Se pueden observar tres partes (dispuestas en columnas): •

Numeración de las líneas, para poder hacer referencia a ellas.

•

Fórmulas lógicas que vamos obteniendo. Las sangrías indican que entramos en un nuevo supuesto (hacia la derecha) o que lo cancelamos (vuelta a la izquierda), configurando lo que llamamos subdeducciones.

•

Justificación de la fórmula obtenida mediante la aplicación de una regla básica a una o más fórmulas anteriores.

3. Editor de fórmulas: se utiliza para insertar nuevas fórmulas dentro de la deducción y decir de qué fórmulas han derivado las mismas. 4. Área de opciones del programa: aquí tenemos los botones que acceden a las diferentes funciones del asistente: Árbol, Aconsejar, Ayuda, Reglas, ... 5. Ventana de información: en este área se muestra información al usuario.

Figura 5: Ventana ADN

ADN únicamente permite la utilización de las reglas básicas. En la ventana de reglas básicas visualizamos las reglas de introducción y eliminación correspondiente al operador lógico que esté seleccionado en la lista superior. En la siguiente figura podemos ver las reglas del disyuntor.

Figura 6: Ventana Reglas Básica

El ADN dispone de una herramienta muy útil a la hora de realizar una deducción. Esta herramienta es el Aconsejador. El aconsejador analiza las fórmulas de la deducción e intenta guiarnos hacia el objetivo o decirnos qué reglas podemos aplicar. No nos llevará siempre a la solución, ya que la deducción natural en lógica de primer orden no es un problema decidible, simplemente es un apoyo. En cualquier momento podemos poner en marcha el aconsejador, y se puede dejar visible durante toda la deducción, con lo que se irá actualizando conforme añadamos o eliminemos fórmulas. En la Figura 7 se puede ver la ventana del aconsejador. En la parte superior de la ventana se muestra una sugerencia de lo que podemos hacer y justo debajo da una pista gráfica con las fórmulas que tenemos en la deducción. Podemos navegar entre todos los consejos generados mediante los botones de Anterior y Siguiente. En la barra de estado del aconsejador podemos ver cuantos consejos se han generado (a la derecha) y cuál estamos visualizando actualmente (a la izquierda). El ADN muestra consejos generados de arriba-abajo (basados en las premisas y fórmulas previas) así como consejos generados de abajo-arriba (basados en la conclusión).

Figura 7: Ventana Aconsejador

Para finalizar la descripción del ADN, en la siguiente figura podemos ver un ejemplo de deducción natural realizada mediante esta herramienta: ∀x P(x) ∨ ∀x Q(x) ⇒ ∀x (P(x) ∨ Q(x))

Figura 8: Ejemplo de Deducción

4. Conclusiones Se ha presentado una herramienta didáctica diseñada ad hoc para la enseñanza de la técnica de deducción natural. Su diseño se ha basado en la observación y el análisis de las dificultades a las que se enfrentaban los estudiantes para aprender y aplicar dicha técnica, así como de los errores habitualmente cometidos. Dicha herramienta se ha desarrollado aprovechando las nuevas tecnologías (efectos multimedia, ejecución a través de la red, tecnología Java y algoritmos robustos). Se ha cuidado mucho tanto el aspecto estético como la facilidad de uso. Bibliografía [Barwise2000] J. Barwise y J. Etchemendy. Language, Proof and Logic. CSLI Publications / Seven Bridges Press, 2000. [Garrido1995] Manuel Garrido, Lógica simbólica. Ed. Tecnos, 3ªedic., 1995 [Gentzen1934] Gerhard Gentzen, Untersuchungen über das logische Schliessen (Investigaciones sobre la deducción lógica), Mathematische Zeitschrift, vol. 39, 1934. [Goldson1993] D. Goldson, S. Reeves and R. Bornat. A Review of Several Programs for the Teaching of Logic. The Computer Journal, vol. 36, nº 4, 1993. [Llorens1996] F. Llorens y Mª J. Castel. Lógica de Primer Orden en las Ingenierías Informáticas. II Jornadas Nacionales de Innovación en las Enseñanzas de las Ingenierías, I.C.E. U.P.M., 1996. [Llorens2000] F. Llorens y S. Mira. ADN (“Natural Deduction Assistant”). Fist International Congress on TOOLS FOR TEACHING LOGIC. Universidad de Salamanca, Junio 2000 [Reeves1990] S. Reeves y M. Clarke, Logic for Computer Science. Ed. AddisonWesley, 1990 [Socher-Ambrosius1997] R. Socher-Ambrosius y P. Johann, Deduction Systems. Ed. Springer-Verlag, 1997 [TTL2000] Fist International Congress on TOOLS FOR TEACHING LOGIC. Universidad de Salamanca, Junio 2000