E: Высокопроизводительная система автоматического доказательства теорем.
E (theorem prover)
E – мощный автоматический доказатель теорем для логики первого порядка. Основан на методе суперпозиции, участвовал в соревнованиях, разработан ТУ Мюнхеном.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
E – высокопроизводительная система доказательства теорем для логики первого порядка с равенством. Она основана на уравнительном исчислении суперпозиций и использует чисто уравнительную парадигму. E был интегрирован в другие системы доказательства теорем и неоднократно занимал лидирующие позиции в соревнованиях по автоматическому доказательству теорем. E разработан Стефаном Шульцем, изначально в группе автоматизированного рассуждения Технического университета Мюнхена, а ныне – в Баден-Вюртембергском кооперативном государственном университете Штутгарта.
E is a high performance theorem prover for full first order logic with equality. It is based on the equational superposition calculus and uses a purely equational paradigm. It has been integrated into other theorem provers and it has been among the best placed systems in several theorem proving competitions. E is developed by Stephan Schulz, originally in the Automated Reasoning Group at TU Munich, now at Baden Württemberg Cooperative State University Stuttgart.
Система
Система основана на уравнительном исчислении суперпозиций. В отличие от большинства современных решателей, реализация действительно использует чисто уравнительную парадигму и моделирует не-уравненческие выводы посредством соответствующих выводов равенства. Значительные нововведения включают совместное переписывание термов (когда множество возможных уравнительных упрощений выполняется за одну операцию), несколько эффективных структур индексирования термов для ускорения вывода, продвинутые стратегии выбора литералов для вывода и различные применения методов машинного обучения для улучшения поведения поиска. Начиная с версии 2.0, E поддерживает многосортную логику. E реализован на языке C и портирован на большинство вариантов UNIX и среду Cygwin. Он распространяется под лицензией GNU GPL.
The system is based on the equational superposition calculus. In contrast to most other current provers, the implementation actually uses a purely equational paradigm, and simulates non equational inferences via appropriate equality inferences. Significant innovations include shared term rewriting (where many possible equational simplifications are carried out in a single operation), several efficient term indexing data structures for speeding up inferences, advanced inference literal selection strategies, and various uses of machine learning techniques to improve the search behaviour. Since version 2.0, E supports many sorted logic. E is implemented in C and portable to most UNIX variants and the Cygwin environment. It is available under the GNU GPL.
Соревнования
Проверка неизменно показывала хорошие результаты в соревновании CADE ATP System Competition, выиграв категорию CNF/MIX в 2000 году и с тех пор постоянно входя в число лучших систем. В 2008 году она заняла второе место. В 2009 году она заняла второе место в категориях FOF (логика первого порядка) и UEQ (логика единичных уравнений) и третье место (после двух версий Vampire) в CNF (клаузальная логика). В 2010 году она повторила результаты в FOF и CNF и получила специальную награду как "лучшая в целом" система. В 2011 году на CASC 23 E она выиграла дивизион CNF и заняла вторые места в UEQ и LTB.
The prover has consistently performed well in the CADE ATP System Competition, winning the CNF/MIX category in 2000 and finishing among the top systems ever since. In 2008 it came in second place. In 2009 it won second place in the FOF (full first order logic) and UEQ (unit equational logic) categories and third place (after two versions of Vampire) in CNF (clausal logic). It repeated the performance in FOF and CNF in 2010, and won a special award as "overall best" system. In the 2011 CASC 23 E won the CNF division and achieved second places in UEQ and LTB.
Приложения
E был интегрирован в несколько других систем доказательства теорем. Вместе с Vampire, SPASS, CVC4 и Z3, он лежит в основе стратегии Sledgehammer в Isabelle. E также является механизмом логического вывода в SInE и LEO II и используется как система клаузулизации для iProver. Области применения E включают рассуждения над большими онтологиями, верификацию программного обеспечения и сертификацию программного обеспечения.
E has been integrated into several other theorem provers. It is, with Vampire, SPASS, CVC4, and Z3, at the core of Isabelle's Sledgehammer strategy. E also is the reasoning engine in SInE and LEO II and used as the clausification system for iProver. Applications of E include reasoning on large ontologies, software verification, and software certification.