macOS
Homebrew已验证 · 100%
brew install vampirelocal Homebrew formula metadata
MacPorts已验证 · 94%
sudo port install vampireMacPorts ports tree · math/vampire/Portfile · 来源: api.github.com
安装
其他安装命令
Linux
Nix已验证 · 92%
nix profile install nixpkgs#vampirenixpkgs package indexes · pkgs/by-name/va/vampire/package.nix · 来源: api.github.com
概览
软件包摘要
High-performance theorem prover
历史
项目历史与用法
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.
项目历史
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.
采用历史
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.
使用方式
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.
来源
安全态势
尚未找到受保护工具覆盖
没有找到 vampire 的匹配本地密钥处理 manifest。Nucleus 软件包元数据仍在此发布，以便未来覆盖拥有稳定的软件包 URL。
安装行为
- 未记录 Homebrew bottle 元数据。
建议审查
在无人值守的代理使用前，请检查该工具是否读取明文凭据、写入远程状态、发布制品或调用插件。
可执行文件
已安装的可执行文件
| 命令 | 类型 | 暴露范围 | 备注 |
|---|---|---|---|
vampire | 可执行文件 | 已索引可执行文件 | 从本地可执行文件索引发现。 |
新鲜度
版本和新鲜度
这些信号区分页生成时间、软件包管理器活动和上游发布比较。只有存在证据 URL 和可比较版本时，才会提示版本落后。
页面生成时间2026-08-03
管理器版本5.0.1
管理器更新时间
本地数据未知
上游不可用
检测到的最新版本未检测到
- OK没有生成新鲜度警告。
安装元数据
软件包元数据
| 软件包键 | brew:vampire |
|---|---|
| 版本 | 5.0.1 |
| 软件包管理器 | Homebrew |
| 主页 | https://vprover.github.io/ |
| 仓库 | https://github.com/vprover/vampire |
| Bottle | 未记录 |
| 服务 | 未声明 |
源数据库匹配
其他软件包管理器记录
匹配项来自外部软件包管理器索引，并与本地 Automic Vault 软件包链接分开显示。
Nix95%
vampire
nix profile install nixpkgs#vampire- normalized package name match
- 匹配方式：Vampire
MacPorts95%
vampire
sudo port install vampire- normalized package name match
- 匹配方式：Vampire
来源线索
由仓库数据生成
此页面由 av-web 从 scripts/generate-pkg-sqlite.py 生成的私有软件包 SQLite 工件提供。
Combined YAML source
View the package source record on GitHub.
使用的来源
- cross-ecosystem install command graph
- curated package history
- external package-manager database matches
- pkg.so package database
- pkgdb category and tag curation