Upír (věta prover) - Vampire (theorem prover)
 | tento článek příliš spoléhá na Reference na primární zdroje. (Květen 2018) (Zjistěte, jak a kdy odstranit tuto zprávu šablony) |
 | tento článek může být pro většinu čtenářů příliš technická na to, aby je pochopili. Prosím pomozte to vylepšit na aby to bylo srozumitelné pro neodborníky, aniž by byly odstraněny technické podrobnosti. (Prosince 2009) (Zjistěte, jak a kdy odstranit tuto zprávu šablony) |
| Původní autoři | Andrej Voronkov[1] |
|---|---|
| Vývojáři | Tým upírů |
| Stabilní uvolnění | 4.4 / 2019-08-24 |
| Úložiště |  |
| Napsáno | C ++ |
| K dispozici v | Upírská licence[2] |
| Typ | Automatizované dokazování věty |
| webová stránka | vprover |
Upír je automatická prověrka věty pro první objednávka klasická logika vyvinut v Ústav výpočetní techniky na University of Manchester. Až do verze 3 byl vyvinut společností Andrej Voronkov společně s Kryštofem Hoderem a dříve s Alexandrem Riazanovem. Od verze 4 se na vývoji podílel širší mezinárodní tým, včetně Laury Kovacs, Giles Regera a Martina Sudy. Od roku 1999 získala nejméně 53 trofejí ve "světovém poháru pro věty" Soutěž systému CADE ATP ) včetně nejprestižnější divize FOF a teoreticky uvažující divize TFA.[3][4]
Pozadí
Upíří jádro implementuje počet objednaných binární rozlišení a superpozice pro řešení rovnosti. Pravidlo rozdělení a rozdělení záporné rovnosti lze simulovat zavedením nových definic predikátů a jejich dynamickým skládáním. A Algoritmus ve stylu DPLL rozdělení je také podporováno. Pro prořezávání prostoru pro vyhledávání se používá řada standardních kritérií redundance a zjednodušujících technik: tautologie vymazání, subsumpce rozlišení, přepisování podle nařízených jednotkových rovností, omezení zásadnosti a neredukovatelnost substitučních termínů. Použitá objednávka redukce je standardní Objednávka Knuth – Bendix.
Řada efektivních indexování techniky se používají k implementaci všech hlavních operací na sadách podmínek a klauzulí. Specializace algoritmu běhu se používá k urychlení shody vpřed.
Přestože jádro systému pracuje pouze s klauzálními normálními formami, komponenta preprocesoru přijímá problém v úplné logické syntaxi prvního řádu, klauzifikuje jej a provede řadu užitečných transformací před předáním výsledku jádru. Když je věta prokázána, systém vytvoří ověřitelný důkaz, který ověří jak klauzifikační fázi, tak vyvrácení konjunktivní normální forma.
Spolu s dokazováním vět má Vampire další související funkce, jako je generování interpolanty.
Spustitelné soubory lze získat na webových stránkách systému.[5] Poněkud zastaralá verze je k dispozici pod GNU Lesser General Public License jako část Sigma KEE.[6]
Reference
- ^ "Dějiny". vprover.github.io. Citováno 2018-05-24.
- ^ „Licence upíra“. vprover.github.io. Citováno 2018-05-24.
- ^ Riazanov, A .; Voronkov, A. (2002). "Návrh a implementace VAMPIRE". AI komunikace. 15 (2-3/2002): 91–110. ISSN 0921-7126.
- ^ Voronkov, A. (1995). „Anatomie upíra“. Journal of Automated Reasoning. 15 (2): 237–265. doi:10.1007 / BF00881918.
- ^ "Upír". vprover.github.io. Citováno 2018-05-24.
- ^ "CVS Info pro projekt sigmakee". sigmakee.cvs.sourceforge.net. Citováno 2018-05-24.
externí odkazy
 | Tento logika související článek je a pahýl. Wikipedii můžete pomoci pomocí rozšiřovat to. |