MINLOG
MINLOG jest asystentem dowodowym opracowanym na Uniwersytecie w Monachium przez zespół Helmuta Schwichtenberga .
MINLOG opiera się na rachunku dedukcji naturalnej pierwszego rzędu . Ma na celu wnioskowanie o obliczalnych funkcjonałach przy użyciu logiki minimalnej , a nie klasycznej lub intuicjonistycznej . Podstawową motywacją stojącą za MINLOG jest wykorzystanie paradygmatu dowodów jako programów do tworzenia i weryfikacji programów. Dowody są w rzeczywistości traktowane jako obiekty pierwszej klasy, które można znormalizować. Jeśli formuła jest egzystencjalna, to jej dowód można wykorzystać do odczytania jej egzemplarza lub odpowiednio zmienić na potrzeby rozwoju programu poprzez transformację dowodu. W tym celu MINLOG wyposażony jest w narzędzia do wyodrębniania programów funkcjonalnych bezpośrednio z terminów dowodowych. Dotyczy to również dowodów niekonstruktywnych, wykorzystujących udoskonalone tłumaczenie A. System jest wspierany przez automatyczne wyszukiwanie dowodu i normalizacja przez ocenę jako wydajne narzędzie do przepisywania terminów .