E

Обзор

E - это средство проверки теорем о насыщении для логики первого и более высокого порядка с равенством. Основное средство проверки работает в четыре этапа: Алгоритм клаузификации преобразует входные данные первого порядка в нормальную форму предложения, так что результирующая формула является невыполнимой, если и только если исходная задача доказуема. (Необязательный) этап предварительной обработки упрощает результирующую клаузальную задачу. Автоматический режим (опционально) анализирует проблему и выбирает подходящие параметры поиска. Алгоритм насыщения, реализующий пример суперпозиционного исчисления, пытается вывести пустое предложение и, следовательно, явное свидетельство невыполнимости задачи. Дополнительные программы предоставляют такие услуги, как проверка доказательств или аксиома

Клаузификация

E преобразует формулы первого порядка в идеально общий банк формул (повторно используя свои зрелые структуры данных с общими терминами). Затем он использует вариант алгоритма клаузификации, описанный в [NW: SmallCNF-2001], без использования передовых методов сколемизации. Совместное представление формулы позволяет очень эффективно вводить и повторно использовать определения - как только определение введено, оно автоматически применяется при каждом появлении синтаксически идентичной формулы.

Исчисление

Основной поиск доказательств выполняется с использованием метода суперпозиционного исчисления, описанного в [BG94] (и, более подробно, в [Schulz:AICOM-2002]). E реализует суперпозицию с отрицательным выбором букв и с учетом равенства, а не с объединяющей парамодуляцией. Он включает в себя ряд методов упрощения, включая безусловное переписывание, включение в категорию, устранение семантической тавтологии и контекстуальное сокращение букв. В нем также используется устранение избыточности AC (на основе информации, полученной перед публикацией, которая позже была задокументирована в [AHL: JSC-2003]) и контролируемое введение определений для независимых частей предложения (что эквивалентно гиперразделению с определениями [RV: IJCAI-2001]). Математический анализ был расширен, чтобы включить дополнительные выводы для логики более высокого порядка, как описано в [VBS:TACAS-2023].

Процедура проверки

E использует вариант алгоритма с заданными предложениями со DISCOUNT [DKS97]. Состояние проверки представлено двумя наборами предложений: набором P обработанных предложений (изначально пустых) и набором U необработанных предложений. Предложения в U ранжируются в соответствии с эвристической оценочной функцией и обрабатываются по порядку. Обработка сначала упростит выбранное предложение g со всеми предложениями в P, затем упростит P с помощью g (переместив все затронутые предложения из P обратно в U), а затем вычислит все прямые следствия между g и P, которые могут быть получены с использованием правил генерирующего вывода (суперпозиция, разложение на множители равенства и разрешение равенства).. Новые предложения упрощены в отношении P и добавлены к U, g добавлено к P.

Эта процедура доказательства отличается от алгоритма с заданным предложением, реализованного в Otter (и многих других разработчиках с тех пор), который также использует U для упрощения. Вариант, который использует E, был впервые популяризирован DISCOUNT, но также лежит в основе Waldmeister. Vampire и SPASS реализуют его в дополнение к своему основному алгоритму.

Эвристика

Основными эвристическими моментами выбора в E являются выбор порядка терминов, который ограничивает выводы и контролирует переписывание, выбор следующего заданного предложения из U и (необязательный) выбор литералов вывода в предложениях, которые содержат по крайней мере один отрицательный литерал.

E позволяет пользователю вручную выбирать тип упорядочения терминов (LPO или KBO), приоритет и веса. Также реализовано большое количество схем формирования приоритета и веса, которые можно выбрать из командной строки или в автоматическом режиме.

Выбор данного предложения контролируется с помощью нескольких приоритетных очередей, из которых предложения выбираются по взвешенной циклической схеме. Каждая очередь сортируется в соответствии с функцией фиксированного приоритета и параметризованной функцией оценки предложений. Функции оценки предложений могут быть целенаправленными, могут фокусироваться на определенных символах и учитывать порядок следования терминов. Вся схема выбора предложений может быть описана с использованием мини-языка, специфичного для предметной области. Автоматический режим автоматически определит проверенную схему для данного класса задач.

Выбор букв управляется с помощью одной из примерно 100 жестко запрограммированных стратегий выбора. В автоматическом режиме проверяющий может выбрать одну из них без вмешательства пользователя.

Структуры данных и алгоритмы

Изначально E не был разработан как инструмент ускорения. Однако он приобрел репутацию быстрого средства доказательства теорем и со временем был дополнен структурами данных, чтобы в какой-то мере оправдать эту репутацию.

E построен на основе полностью разделяемых терминов, т.е. каждый отдельный термин представлен в банке терминов только один раз. Таким образом, весь набор терминов состоит из ряда взаимосвязанных направленных ациклических графов. Память терминов управляется простым сборщиком мусора с пометкой и очисткой.

Безусловное (прямое) переписывание с использованием единичных предложений осуществляется с использованием совершенных деревьев распознавания с ограничениями по размеру и возрасту. Всякий раз, когда обнаруживается возможное упрощение, оно добавляется в качестве ссылки для перезаписи в банк терминов. В результате не только термины, но и этапы перезаписи становятся общими.

Выделение объектов и контекстное буквальное сокращение (также известное как разрешение выделения объектов) поддерживаются с помощью векторной индексации объектов [Schulz: FVI-2013].

Наложение и обратная перезапись используют индексацию отпечатков пальцев [Schulz: IJCAR-2012], новую технологию, сочетающую идеи векторной индексации объектов и индексации контуров.

Наконец, LPO и KBO реализованы с использованием элегантных и эффективных алгоритмов, разработанных Берндом Лехнером в [Loechner:IJAIT-2006] [Loechner:JAR-2006].

Реализация

E реализован в ANSI-C, в основном в соответствии со стандартом 1989 года. Для этого требуется расширение long long с C-99.

По умолчанию он использует набор инструментов GNU, но также был успешно собран с использованием нескольких различных сред компиляции.