MINLOG

MINLOG es un asistente de demostración desarrollado en la LMU de Múnich por el equipo de Helmut Schwichtenberg . ^{[ 1 ] [ 2 ]}

MINLOG se basa en el cálculo de deducción natural de primer orden . Su objetivo es razonar sobre funcionales computables , utilizando lógica mínima en lugar de lógica clásica o intuicionista . La principal motivación de MINLOG es aprovechar el paradigma de las pruebas como programas para el desarrollo y la verificación de programas. De hecho, las pruebas se tratan como objetos de primera clase, que pueden normalizarse. Si una fórmula es existencial, su prueba puede utilizarse para obtener una instancia de la misma o modificarse adecuadamente para el desarrollo del programa mediante la transformación de pruebas. Para ello, MINLOG cuenta con herramientas para extraer programas funcionales directamente de los términos de las pruebas. Esto también se aplica a las pruebas no constructivas, utilizando una traducción A refinada . El sistema se apoya en la búsqueda automática de pruebas y la normalización mediante evaluación como un dispositivo eficiente para la reescritura de términos .

• Página principal de MINLOG