En la primera parte de la clase de hoy del curso de Razonamiento automático se han comentado el uso de editores lógicos, distintos de Isabelle/HOL, que facilitan y corrigen la escritura de demostraciones por deducción natural o mediante secuentes.

El primero que se ha presentado es Pandora. Es un editor para la deducción natural. Se han realizado las demostraciones que se muestran en este vídeo. Un libro usando Pandora es Reasoned programming.

El segundo que se ha presentado es Conan. También es un editor para deducción natural. Se han realizado las mismas demostraciones que con Pandora. La descripción de Conan se encuentra en Proof editor for natural deduction in first-order logic.

El tercero que se ha presentado es Logitext. Es un un editor para el cálculo de secuentes. Se han realizado las demostraciones propuestas en su tutorial.

Finalmente se ha presentado APLI2 (APLIcación de Ayuda Para Lógica Informática) que contiene una colección de problemas para traducir argumentos del lenguaje natural al lenguaje de la lógica de primer orden y automáticamente corrige la traducción.