726:
654:
300:
669:
65:
24:
167:
461:, the preprocessor component accepts a problem in the full first-order logic syntax, clausifies 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 clausification phase and the refutation of the
478:
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.
386:
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
791:
375:
185:
811:
767:
796:
786:
37:
801:
436:
419:
splitting is also supported. A number of standard redundancy criteria and simplification techniques are used for pruning the search space:
710:
129:
451:
221:
203:
148:
51:
101:
86:
79:
760:
108:
582:
733:
391:, the "world cup for theorem provers", including the most prestigious FOF division and the theory-reasoning TFA division.
43:
411:(for handling equality). The splitting rule and negative equality splitting can be simulated by the introduction of new
279:
115:
753:
388:
263:
97:
75:
400:
364:
336:
725:
703:
379:
462:
458:
408:
806:
428:
122:
696:
469:
331:
599:
427:
resolution, rewriting by ordered unit equalities, basicness restrictions and irreducibility of
559:
420:
412:
404:
368:
737:
680:
591:
577:
547:
468:
Along with proving theorems, Vampire has other related functionalities such as generating
383:
371:
242:
299:
653:
447:
416:
780:
443:
603:
432:
324:
64:
475:
249:
237:
563:
424:
446:
techniques are used to implement all major operations on sets of terms and
668:
521:
496:
595:
288:
313:
676:
160:
58:
17:
647:
617:
347:
792:
Department of
Computer Science, University of Manchester
741:
684:
415:
definitions and dynamic folding of such definitions. A
181:
550:(2002). "The design and implementation of VAMPIRE".
342:
330:
319:
309:
278:
262:
248:
236:
176:
may be too technical for most readers to understand
457:Although the kernel of the system works only with
761:
704:
8:
52:Learn how and when to remove these messages
768:
754:
711:
697:
652:
298:
233:
222:Learn how and when to remove this message
204:Learn how and when to remove this message
188:, without removing the technical details.
149:Learn how and when to remove this message
454:is used to accelerate forward matching.
488:
382:. Up to Version 3, it was developed by
85:Please improve this article by adding
186:make it understandable to non-experts
7:
722:
720:
665:
663:
812:Free and open-source software stubs
740:. You can help Knowledge (XXG) by
683:. You can help Knowledge (XXG) by
580:(1995). "The anatomy of vampire".
431:terms. The reduction ordering on
403:implements the calculi of ordered
14:
452:Run-time algorithm specialisation
33:This article has multiple issues.
787:Theorem proving software systems
724:
667:
522:"Vampire Licence (Modified BSD)"
165:
63:
22:
797:Free software programmed in C++
41:or discuss these issues on the
802:Software using the BSD license
583:Journal of Automated Reasoning
376:Department of Computer Science
1:
734:free and open-source software
98:"Vampire" theorem prover
87:secondary or tertiary sources
389:CADE ATP System Competition
828:
719:
662:
337:Automated theorem proving
274:
258:
459:conjunctive normal forms
380:University of Manchester
365:automatic theorem prover
463:conjunctive normal form
679:-related article is a
442:A number of efficient
74:relies excessively on
437:Knuth–Bendix ordering
269:4.5.1 / 2020-07-15
558:(2–3/2002): 91–110.
417:DPLL-style algorithm
596:10.1007/BF00881918
238:Original author(s)
749:
748:
692:
691:
622:vprover.github.io
552:AI Communications
526:vprover.github.io
501:vprover.github.io
405:binary resolution
374:developed in the
358:
357:
323:Vampire Modified
232:
231:
224:
214:
213:
206:
159:
158:
151:
133:
56:
819:
770:
763:
756:
728:
721:
713:
706:
699:
671:
664:
656:
651:
650:
648:Official website
633:
632:
630:
628:
614:
608:
607:
574:
568:
567:
543:
537:
536:
534:
532:
518:
512:
511:
509:
507:
493:
435:is the standard
354:
351:
349:
302:
297:
294:
292:
290:
234:
227:
220:
209:
202:
198:
195:
189:
169:
168:
161:
154:
147:
143:
140:
134:
132:
91:
67:
59:
48:
26:
25:
18:
827:
826:
822:
821:
820:
818:
817:
816:
777:
776:
775:
774:
718:
717:
660:
646:
645:
642:
637:
636:
626:
624:
616:
615:
611:
576:
575:
571:
545:
544:
540:
530:
528:
520:
519:
515:
505:
503:
495:
494:
490:
485:
397:
384:Andrei Voronkov
372:classical logic
346:
305:
287:
270:
243:Andrei Voronkov
228:
217:
216:
215:
210:
199:
193:
190:
182:help improve it
179:
170:
166:
155:
144:
138:
135:
92:
90:
84:
80:primary sources
68:
27:
23:
12:
11:
5:
825:
823:
815:
814:
809:
804:
799:
794:
789:
779:
778:
773:
772:
765:
758:
750:
747:
746:
729:
716:
715:
708:
701:
693:
690:
689:
672:
658:
657:
641:
640:External links
638:
635:
634:
609:
590:(2): 237–265.
569:
546:Riazanov, A.;
538:
513:
487:
486:
484:
481:
396:
393:
356:
355:
344:
340:
339:
334:
328:
327:
321:
317:
316:
311:
307:
306:
304:
303:
284:
282:
276:
275:
272:
271:
268:
266:
264:Stable release
260:
259:
256:
255:
252:
246:
245:
240:
230:
229:
212:
211:
173:
171:
164:
157:
156:
71:
69:
62:
57:
31:
30:
28:
21:
13:
10:
9:
6:
4:
3:
2:
824:
813:
810:
808:
805:
803:
800:
798:
795:
793:
790:
788:
785:
784:
782:
771:
766:
764:
759:
757:
752:
751:
745:
743:
739:
736:article is a
735:
730:
727:
723:
714:
709:
707:
702:
700:
695:
694:
688:
686:
682:
678:
673:
670:
666:
661:
655:
649:
644:
643:
639:
623:
619:
613:
610:
605:
601:
597:
593:
589:
585:
584:
579:
573:
570:
565:
561:
557:
553:
549:
542:
539:
527:
523:
517:
514:
502:
498:
492:
489:
482:
480:
477:
473:
471:
466:
464:
460:
455:
453:
449:
445:
440:
438:
434:
430:
426:
422:
418:
414:
410:
409:superposition
406:
402:
394:
392:
390:
385:
381:
377:
373:
370:
366:
362:
353:
345:
341:
338:
335:
333:
329:
326:
322:
318:
315:
312:
308:
301:
296:
286:
285:
283:
281:
277:
273:
267:
265:
261:
257:
253:
251:
247:
244:
241:
239:
235:
226:
223:
208:
205:
197:
194:December 2009
187:
183:
177:
174:This article
172:
163:
162:
153:
150:
142:
131:
128:
124:
121:
117:
114:
110:
107:
103:
100: –
99:
95:
94:Find sources:
88:
82:
81:
77:
72:This article
70:
66:
61:
60:
55:
53:
46:
45:
40:
39:
34:
29:
20:
19:
16:
742:expanding it
731:
685:expanding it
674:
659:
625:. Retrieved
621:
612:
587:
581:
578:Voronkov, A.
572:
555:
551:
548:Voronkov, A.
541:
529:. Retrieved
525:
516:
504:. Retrieved
500:
491:
474:
470:interpolants
467:
456:
441:
429:substitution
398:
360:
359:
320:Available in
254:Vampire team
250:Developer(s)
218:
200:
191:
175:
145:
136:
126:
119:
112:
105:
93:
73:
49:
42:
36:
35:Please help
32:
15:
807:Logic stubs
476:Executables
425:subsumption
369:first-order
325:BSD Licence
781:Categories
627:2 November
531:2 November
483:References
423:deletion,
399:Vampire's
395:Background
310:Written in
280:Repository
109:newspapers
76:references
38:improve it
618:"Vampire"
564:0921-7126
497:"History"
421:tautology
413:predicate
44:talk page
444:indexing
295:/vampire
293:/vprover
139:May 2018
604:1541122
448:clauses
378:at the
361:Vampire
350:.github
348:vprover
343:Website
180:Please
123:scholar
602:
562:
506:24 May
401:kernel
363:is an
289:github
125:
118:
111:
104:
96:
732:This
677:logic
675:This
600:S2CID
433:terms
130:JSTOR
116:books
738:stub
681:stub
629:2022
560:ISSN
533:2022
508:2018
407:and
367:for
332:Type
291:.com
102:news
592:doi
352:.io
314:C++
184:to
78:to
783::
620:.
598:.
588:15
586:.
556:15
554:.
524:.
499:.
472:.
465:.
450:.
439:.
89:.
47:.
769:e
762:t
755:v
744:.
712:e
705:t
698:v
687:.
631:.
606:.
594::
566:.
535:.
510:.
225:)
219:(
207:)
201:(
196:)
192:(
178:.
152:)
146:(
141:)
137:(
127:·
120:·
113:·
106:·
83:.
54:)
50:(
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
