Кіріспе

E — теңдікпен толық бірінші реттік логика үшін жоғары өнімділіктегі теореманы дәлелдейтін жүйе. Ол теңдеулік суперпозициялық есептеуге негізделген және таза теңдеулік парадигманы қолданады. E басқа теореманы дәлелдейтін жүйелерге интеграцияланған және бірнеше теореманы дәлелдеу жарыстарында үздік нәтижелер көрсеткен. E-ді Стефан Шульц жасаған, бұрын Мюнхен техникалық университетінің Автоматтандырылған қорыту тобында, қазір Баден-Вюртемберг кооперативтік мемлекеттік университетінде (Штутгарт) жұмыс істейді.

Жүйе

Жүйе теңдеулік суперпозициялық есептеу негізінде құрылған. Көптеген қазіргі дәлелдеушілерден өзгеше, іске асыру шын мәнінде таза теңдеулік парадигманы қолданады және тиісті теңдік тұжырымдамалары арқылы теңдеулік емес тұжырымдамаларды модельдейді. Маңызды жаңалықтарға ортақ терминнің қайта жазылуы (бір операцияда көптеген мүмкін теңдеулік жеңілдетулер орындалады), тұжырымдамаларды жылдамдату үшін бірнеше тиімді терминнің индекстеу дерек құрылымдары, жетілдірілген тұжырымдамалық әрекеттерді таңдау стратегиялары және іздеу мінез-құлқын жақсарту үшін машиналық оқыту техникаларын қолдану кіреді. 2.0 нұсқасынан бастап E көп сұрыпталған логиканы қолдайды. E C тілінде іске асырылған және көптеген UNIX нұсқаларында және Cygwin ортасында қолданылуы мүмкін. Ол GNU GPL лицензиясы бойынша қолжетімді.

Жарыстар

Проверник CADE ATP System Competition-де үнемі жақсы нәтижелер көрсетіп келеді, 2000 жылы CNF/MIX санатында жеңімпаз атанды және содан бері үздік жүйелердің қатарында. 2008 жылы ол екінші орынды иеленді. 2009 жылы FOF (толық бірінші реттік логика) және UEQ (бірлік теңдеу логикасы) санаттарында екінші орынды, ал CNF (клаузалды логика) санатында үшінші орынды (Vampire-дің екі нұсқасынан кейін) жеңіп алды. 2010 жылы ол FOF және CNF көрсеткіштерін қайталады және "жалпы ең жақсы" жүйе ретінде арнайы сыйлыққа ие болды. 2011 жылы CASC 23 E CNF дивизионында жеңімпаз атанды және UEQ және LTB санаттарында екінші орынды иеленді.

Қолданбалар

E бірнеше басқа теореманы дәлелдейтін жүйелерге енгізілген. E, Vampire, SPASS, CVC4 және Z3 сияқты, Isabelle жүйесіндегі Sledgehammer стратегиясының ядросы болып табылады. E сонымен қатар SInE және LEO II жүйелеріндегі логикалық қорытынды шығару механизмі болып табылады және iProver үшін клаузаға айналдыру жүйесі ретінде пайдаланылады. E-нің қолданылу салаларына үлкен онтологиялар бойынша қорытынды шығару, бағдарламалық жасақтаманы тексеру және бағдарламалық жасақтаманы сертификаттау кіреді.