Vampire – бірінші реттік логика үшін автоматты теореманы дәлелдейтін жүйе. Манчестер университетінде жасалған, CADE ATP жарысында 53 жүлде жеңіп алған.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Кіріспе
Vampire – Манчестер университетінің Компьютерлік ғылым кафедрасында әзірленген бірінші реттік классикалық логиканың автоматты теореманы дәлелдейтін жүйе. 3-ші нұсқаға дейін оны Андрей Воронков Кристоф Ходермен және одан бұрын Александр Рьязановпен бірге әзірлеген. 4-ші нұсқадан бастап, дамуға Лаура Ковакс, Джайлс Регер және Мартин Суда сияқты халықаралық команда кеңінен қатысты. 1999 жылдан бері ол «теореманы дәлелдеушілер үшін әлем кубогы» саналатын CADE ATP System Competition-да кем дегенде 53 жүлде жеңіп алды, оның ішінде ең беделді 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 стиліндегі алгоритмді бөлу де қолдау көрсетіледі. Іздеу кеңістігін қысқарту үшін бірқатар стандартты артық критерийлер мен оңайлату техникалары қолданылады: тавтологияны жою, субсумпциялық шешімдеу, реттелген бірлік теңдіктерімен қайта жазу, негізділік шектеулері және алмастыру шарттарының ирредуктибелдігі. Шарттар бойынша азайту реті стандартты Knuth–Bendix реті болып табылады. Шарттар мен клаузалар жиындарына қатысты барлық негізгі операцияларды іске асыру үшін бірқатар тиімді индекстеу техникалары қолданылады. Алдын-ала сәйкестікті үдету үшін орындалу уақытында алгоритмді мамандандыру қолданылады. Жүйенің ядросы тек конъюнктивті қалыпты формалармен жұмыс істейді, бірақ препроцессор компоненті толық бірінші реттік логикалық синтаксистегі мәселені қабылдайды және нәтижені ядроға жібермес бұрын бірқатар пайдалы түрлендірулерді орындайды. Теорема дәлелденген кезде, жүйе конъюнктивті қалыпты форманың фазасын да, жоққа шығаруын да растайтын тексерілетін дәлелді ұсынады. Теоремаларды дәлелдеумен қатар, 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.