Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Введение
Vampire – это автоматический теоремодоказатель для классической логики первого порядка, разработанный в Департаменте компьютерных наук Манчестерского университета. До версии 3 он разрабатывался Андреем Воронковым совместно с Кристофом Ходером и ранее с Александром Рязановым. Начиная с версии 4, в разработке участвует более широкая международная команда, включающая Лауру Ковач, Джайлза Регера и Мартина Суду. С 1999 года Vampire завоевал как минимум 53 приза в соревновании CADE ATP System Competition, известном как "чемпионат мира для теоремодоказателей", включая престижнейшие категории FOF и TFA (теоретическое рассуждение).
Vampire is an automatic theorem prover for first order classical logic developed in the Department of Computer Science at the University of Manchester. Up to Version 3, it was developed by Andrei Voronkov together with Kryštof Hoder and previously with Alexandre Riazanov. Since Version 4, the development has involved a wider international team including Laura Kovacs, Giles Reger, and Martin Suda. Since 1999 it has won at least 53 trophies in the CADE ATP System Competition, the "world cup for theorem provers", including the most prestigious FOF division and the theory reasoning TFA division.
Предыстория
Ядро Vampire реализует исчисления упорядоченного бинарного разрешения и суперпозиции (для обработки равенства). Правило расщепления и расщепление отрицательных равенств могут быть смоделированы путем введения новых определений предикатов и динамического сворачивания этих определений. Также поддерживается расщепление в стиле DPLL. Для сокращения пространства поиска используется ряд стандартных критериев избыточности и техник упрощения: удаление тавтологий, разрешение с субумпцией, переписывание по упорядоченным единичным равенствам, ограничения на основность и нередуцируемость подстановочных термов. Порядок редукции термов – стандартный порядок Кнута — Бендикса. Для реализации всех основных операций над множествами термов и клауз используются различные эффективные методы индексации. Специализация алгоритма во время выполнения используется для ускорения прямого сопоставления. Хотя ядро системы работает только с конъюнктивными нормальными формами, компонент предварительной обработки принимает задачу в полном синтаксисе логики первого порядка и выполняет ряд полезных преобразований перед передачей результата ядру. Когда теорема доказана, система генерирует верифицируемое доказательство, которое подтверждает как фазу, так и опровержение конъюнктивной нормальной формы. Помимо доказательства теорем, Vampire обладает другими связанными функциями, такими как генерация интерполянтов. Исполняемые файлы доступны на веб-сайте системы. По состоянию на ноябрь 2020 года Vampire распространяется под модифицированной версией лицензии BSD 3, которая явно разрешает коммерческое использование. Предыдущие версии были доступны под проприетарной некоммерческой лицензией.
Vampire's kernel implements the calculi of ordered binary resolution and superposition (for handling equality). The splitting rule and negative equality splitting can be simulated by the introduction of new predicate definitions and dynamic folding of such definitions. A DPLL style algorithm splitting is also supported. A number of standard redundancy criteria and simplification techniques are used for pruning the search space: tautology deletion, subsumption resolution, rewriting by ordered unit equalities, basicness restrictions and irreducibility of substitution terms. The reduction ordering on terms is the standard Knuth–Bendix ordering. A number of efficient indexing techniques are used to implement all major operations on sets of terms and clauses. Run time algorithm specialisation is used to accelerate forward matching. Although the kernel of the system works only with conjunctive normal forms, the preprocessor component accepts a problem in the full first order logic syntax, it and performs a number of useful transformations before passing the result to the kernel. When a theorem is proven, the system produces a verifiable proof, which validates both the phase and the refutation of the conjunctive normal form. Along with proving theorems, Vampire has other related functionalities such as generating interpolants. Executables can be obtained from the system website. As of November 2020, Vampire is released under a modified version of the BSD 3 clause licence that explicitly permits commercial use. Previous versions were available under a proprietary non commercial licence.