macOS
Homebrewvérifié · 100%
brew install vampirelocal Homebrew formula metadata
MacPortsvérifié · 94%
sudo port install vampireMacPorts ports tree · math/vampire/Portfile · Source: api.github.com
brew / rang 9502
Installer vampire avec Homebrew, MacPorts, Nix
Consultez les chemins d'installation, exécutables, métadonnées et notes de sécurité de vampire pour les workflows d'agents IA.
installation
Commandes d'installation supplémentaires
Linux
Nixvérifié · 92%
nix profile install nixpkgs#vampirenixpkgs package indexes · pkgs/by-name/va/vampire/package.nix · Source: api.github.com
aperçu
Résumé du paquet
High-performance theorem prover
Liens du projet
Commandes et alias
- vampire
historique
Historique du projet et usages
Vampire is a high-performance automated theorem prover whose lineage goes back to Andrei Voronkov's theorem-proving work in Novosibirsk around 1990 and an earlier Lisp predecessor called Drakosha. The Vampire project itself began at Uppsala University in 1994 after Voronkov's visit to Bull Research Lab. Its first C++ incarnation was used for experiments with code trees and early competition work against SETHEO.
Historique du projet
The second major incarnation appeared in Uppsala and then moved to the University of Manchester, developed from 1998 by Voronkov and Alexandre Riazanov and later maintained by Voronkov. The project history says this line of Vampire began winning CASC competitions in 1999. A third reincarnation started in 2008 with Kryštof Hoder, reusing some preprocessing code but rewriting the resolution and superposition engine; the 2009 competition version combined second- and third-generation components through scripts named Dracula and Drakosha. From 2014, a broader team took over active development, with important contributions in program analysis, interpolation, and symbol elimination from Laura Kovacs and later work centered around Manchester, Vienna, and other automated-reasoning groups.
Historique d'adoption
Competition history is central to Vampire's reputation. The official trophy page says Vampire has won at least one division of CASC, the world cup in theorem proving, since 1999, and as of the March 2026 update had won 78 titles, more than any other prover. In 2025 it achieved a CASC clean sweep, winning all eight theorem-proving divisions that year. That record explains why Vampire is packaged not as a general developer utility but as a specialized science/formal-methods tool: it is a benchmark-grade prover used by researchers and verification systems that need aggressive saturation-based reasoning.
Modes d'utilisation
Vampire's niche is first-order automated theorem proving, but its feature set has expanded beyond pure theorem proving. The project site describes support for disproving non-theorems, finite model building, combinations of theories such as arithmetic, arrays, and datatypes, SMT-LIB input, portfolio and multicore modes, proof output, finite models, and increasing higher-order and inductive reasoning support. In package usage, users typically invoke the `vampire` binary on TPTP or SMT-LIB problems, tune modes such as CASC-style strategy selection, and integrate it into verification, formal methods, knowledge representation, or theorem-proving research workflows.
Sources
posture de sécurité
Aucune couverture d'outil protégé trouvée pour le moment
Aucun manifest local de gestion des secrets correspondant n'a été trouvé pour vampire. Les métadonnées de paquet Nucleus restent publiées ici afin que la couverture future dispose d'une URL stable.
Comportement d'installation
- Aucune métadonnée de bottle Homebrew n’a été enregistrée.
Revue recommandée
Avant une utilisation sans surveillance par un agent, vérifiez si l'outil lit des identifiants en clair, écrit un état distant, publie des artefacts ou lance des plugins.
exécutables
Exécutables installés
| Commande | Type | Exposition | Note |
|---|---|---|---|
vampire | exécutable | exécutable indexé | Découvert depuis l'index local des exécutables. |
fraîcheur
Version et fraîcheur
Ces signaux séparent l'âge de génération de la page, l'activité du gestionnaire de paquets et la comparaison avec les versions amont. Un retard de version n'est signalé que lorsqu'une URL de preuve et des versions comparables sont présentes.
page générée2026-08-03
version du gestionnaire5.0.1
gestionnaire mis à jour
données localesinconnu
amontnon disponible
dernière version détectéenon détecté
- OKAucun avertissement de fraîcheur n'a été généré.
métadonnées d'installation
Métadonnées du paquet
| Clé du paquet | brew:vampire |
|---|---|
| Version | 5.0.1 |
| Gestionnaire de paquets | Homebrew |
| Page d'accueil | https://vprover.github.io/ |
| Dépôt | https://github.com/vprover/vampire |
| Bouteille | non enregistré |
| Service | aucun déclaré |
correspondances dans les bases sources
Autres enregistrements de gestionnaires de paquets
Les correspondances proviennent d’index externes de gestionnaires de paquets et restent séparées des liens de paquets Automic Vault locaux.
Nix95%
vampire
nix profile install nixpkgs#vampire- normalized package name match
- Correspondance par : Vampire
MacPorts95%
vampire
sudo port install vampire- normalized package name match
- Correspondance par : Vampire
piste source
Généré depuis les données du dépôt
Cette page est servie par av-web depuis l'artéfact SQLite privé des paquets généré par scripts/generate-pkg-sqlite.py.
Combined YAML source
View the package source record on GitHub.
Sources utilisées
- cross-ecosystem install command graph
- curated package history
- external package-manager database matches
- pkg.so package database
- pkgdb category and tag curation