МИНЛОГ
MINLOG — помощник по доказательству, разработанный в Мюнхенском университете командой Хельмута Швихтенберга .
MINLOG основан на первого порядка исчислении естественного вывода . Он предназначен для рассуждений о вычислимых функционалах , используя минимальную , а не классическую или интуиционистскую логику . Основной мотивацией MINLOG является использование парадигмы «доказательства как программы» для разработки и проверки программ. Фактически доказательства рассматриваются как первоклассные объекты, которые можно нормализовать. Если формула является экзистенциальной, то ее доказательство можно использовать для считывания ее экземпляра или изменить соответствующим образом для разработки программы путем преобразования доказательства. С этой целью MINLOG оснащен инструментами для извлечения функциональных программ непосредственно из условий доказательства. Это относится и к неконструктивным доказательствам с использованием уточненного А-перевода . Система поддерживается автоматическим поиском доказательств и нормализацией путем оценки как эффективное устройство переписывания терминов .