MINLOG es un asistente de prueba desarrollado en la Universidad de Munich por el equipo de Helmut Schwichtenberg .
MINLOG se basa en el cálculo de deducción natural de primer orden . Su objetivo es razonar sobre funcionales computables , utilizando una lógica mínima en lugar de clásica o intuicionista.. La principal motivación detrás de MINLOG es explotar el paradigma de pruebas como programas para el desarrollo y verificación de programas. Las pruebas son, de hecho, tratadas como objetos de primera clase, que pueden normalizarse. Si una fórmula es existencial, entonces su prueba se puede usar para leer una instancia de ella o se puede cambiar apropiadamente para el desarrollo del programa mediante la transformación de la prueba. Para ello, MINLOG está equipado con herramientas para extraer programas funcionales directamente de los términos de prueba. Esto también se aplica a las pruebas no constructivas, utilizando una traducción A refinada . El sistema es compatible con la búsqueda automática de pruebas y la normalización mediante evaluación como un dispositivo eficaz de reescritura de términos .