MINLOG - MINLOG - Wikipedia
MINLOG Бұл дәлелдеу көмекшісі командасы Мюнхен университетінде әзірледі Гельмут Швихтенберг.
MINLOG негізделген бірінші тапсырыстабиғи шегерім есептеу. Бұл туралы ойлануға арналған есептелетін функционалдар, қолдану минималды гөрі классикалық немесе интуициялық логика. MINLOG-тің негізгі мотивациясы - бағдарлама жасау мен бағдарламаны тексеру үшін бағдарламалар дәлелі парадигмасын пайдалану. Дәлелдемелер, шын мәнінде, қалыпқа келтіруге болатын бірінші класты объектілер ретінде қарастырылады. Егер формула экзистенциалды болса, онда оның дәлелі оның данасын оқып шығу үшін пайдаланылуы мүмкін немесе дәлелдеулер түрлендіру арқылы бағдарламаны әзірлеу үшін сәйкесінше өзгертілуі мүмкін. Осы мақсатта MINLOG функционалдық бағдарламаларды тікелей дәлелдемелерден шығаруға арналған құралдармен жабдықталған. Бұл нақтыланған конструктивті емес дәлелдерге қатысты А аударма. Жүйеге автоматты дәлелдеу іздеуі қолдау көрсетеді бағалау арқылы қалыпқа келтіру тиімді ретінде мерзімді қайта жазу құрылғы.