Vampire 定理证明器The Vampire Theorem Prover是自动定理证明领域中最具代表性的工具之一。它解决的任务可以概括为给定一组一阶逻辑公式自动判断这些公式是否不可满足并在不可满足时返回一条可以复核的反证。无论是数学定理的机器证明还是程序验证、硬件验证和形式化方法中的证明义务Vampire 都经常作为后台证明引擎出现。对于刚开始接触自动定理证明的人来说它的门槛主要不在安装而在理解“反证法”这个核心思路以及 TPTP 输入格式的书写规范。这篇文章从使用者的角度出发先用一个最小例子跑通完整流程再解释 Vampire 背后的核心机制、常用命令行参数、输出状态的含义以及在 Why3、Isabelle/HOL 等验证工具链中的接入方式。最后给出排错链路和可复用清单。建议你准备一台 Linux 机器或者安装好 WSL 的 Windows 机器亲自动手跑一遍这些例子。1. 一阶逻辑、不可满足性与反证法Vampire 究竟在解什么题1.1 先看一个真实的使用场景假设你在做一个程序验证任务。代码的前置条件是x 0循环执行完后得到x 0现在需要证明某个后置属性。把程序语义翻译成一阶逻辑公式后验证任务通常变成把前置条件和程序语义写成一组公理。把要证明的目标写成 conjecture。交给证明器判断目标是否一定成立。这类任务如果只靠人工证明规模大了之后很难保证没有遗漏。Vampire 这类自动定理证明器就是用来把“判断目标是否成立”这件事自动化。从逻辑角度看Vampire 处理的对象非常明确一阶逻辑公式集。它不直接理解 Java、C 或 TLA但它能处理这些工具翻译出来的底层逻辑公式。1.2 为什么主流证明器都采用反证法很多人第一次使用 Vampire 时会觉得“它怎么不直接证明目标成立”。实际上主流自动定理证明器普遍采用反证法思路。要证明前提A蕴含结论B等价于证明A 且 ¬B不可满足。也就是说不存在任何解释能让所有前提为真同时让结论的否定也为真。如果这样的解释不存在那么结论在所有满足前提的解释中都为真结论自然成立。归结演算和叠加演算都建立在不可满足性语义之上。Vampire 会把输入中的 conjecture 自动取反加入公式集然后反复应用推理规则直到推出空子句。空子句表示矛盾输出Refutation found就代表反证成功。1.3 Vampire 能处理哪些逻辑范围Vampire 的核心范围是一阶逻辑First-Order LogicFOL。带等式的一阶逻辑这也是它在工程场景中特别重要的原因。类型化一阶逻辑对应 TPTP 中的tff子语言。通过 SMT-LIB 输入格式接入部分带算术背景的验证场景。它不属于交互式定理证明器。Isabelle/HOL 和 Coq 也支持定理证明但它们的核心是人与机器合作逐条应用策略逐步构建证明。Vampire 更接近 SMT 求解器但与 Z3、CVC4/5 这类 SMT 求解器又有区别。SMT 求解器擅长处理位向量、整数、实数、数组等理论组合通常面向软件验证场景。Vampire 的核心更偏纯一阶逻辑和高性能的归结、叠加演算在 TPTP 题库和 CASC 比赛中长期处于第一梯队。两者有重叠也各有强项。1.4 一个直观的最小输入输出Vampire 的最小输入文件可以简单到只有几个公式。例如下面这个经典三段论fof(ax1, axiom, man(socrates)). fof(ax2, axiom, ! [X] : (man(X) mortal(X))). fof(conj, conjecture, mortal(socrates)).保存为socrates.p运行vampire socrates.p在正常结果中可以看到类似Refutation found的结论。这个例子虽然简单但已经包含了 TPTP 格式、conjecture 处理、反证法三个关键概念。后面会逐步展开。要理解 Vampire首先要理解为什么它能用一个极小输入判断出“苏格拉底会死”。2. 核心机制归结、叠加演算与 AVATAR 为什么高效2.1 归结一阶逻辑最经典的推理规则归结原理由 Robinson 在 1965 年提出是早期自动定理证明的基石。它的基本思想是两个子句如果包含互补文字比如P(X)和¬P(a)通过合一操作让它们一致就可以消去这对互补文字生成一个新子句。例如子句1: ¬man(X) | mortal(X) 子句2: man(socrates)对X做合一替换X socrates得到新子句mortal(socrates)如果再把¬mortal(socrates)加入就能推导出空子句从而得到矛盾。Vampire 并不只使用朴素归结。它会对公式先做子句化把一阶公式转换为合取范式然后用索引结构加速子句匹配用化简、删除、包含关系等方式降低冗余推理。2.2 等式为什么需要叠加演算如果只有谓词而没有等式归结已经足够。但实际数学和验证场景大量使用。例如a b、f(x) x 1需要专门的规则处理。叠加演算Superposition Calculus可以理解为带等词的归结和参数化规则的整合。它把等式信息组织成重写规则在推导过程中对子句做规范化。类似 Knuth-Bendix 完成化的思想系统会尽量把等式定向为可重写规则然后反复化简子句减少需要探索的搜索空间。这也是 Vampire 在实际问题中表现好的关键点之一。很多验证问题本质上就是等式推理问题直接用纯归结会慢很多叠加和重写能显著压缩子句规模。2.3 AVATAR用 SAT 模型引导子句选择Vampire 一个很有代表性的设计是 AVATAR 架构。它的全称可以理解为一种把 SAT 求解器与一阶推理结合起来的技术。AVATAR 的核心思路是把一阶子句中的文字抽象成命题变量。将子句转换成命题子句交给 SAT 求解器处理。SAT 求解器给出一个命题模型表示“哪些文字在当前假设中为真”。Vampire 根据这个模型生成一个相对关注的子句子集做一阶推理。当一阶推理发现矛盾时把矛盾对应的文字组合作为引理反馈给 SAT 求解器SAT 再切换到下一个命题模型。这种做法的好处是一阶搜索不再完全盲目而是由命题层面的模型指导。遇到大公理集时AVATAR 能避免同时激活所有子句减少无效推理。需要说明的是AVATAR 不是对所有问题都必要。某些小问题或者特殊理论下关闭 AVATAR 反而更快。这也是 Vampire 提供大量策略参数的原因。2.4 策略调度把多组参数按时间依次执行Vampire 的策略调度机制本质上是一个预设的参数组合队列。不同问题适用不同策略有的问题适合开启 AVATAR有的问题适合做更强力的化简有的问题可能需要更激进的子句删除。在 CASC 比赛模式下Vampire 通常会在限时内依次尝试多个策略。这也是为什么同一个问题直接跑默认设置和用--mode casc跑结果可能不同。理解策略调度并不需要一开始就掌握所有参数。第一步是认识--time_limit、--memory_limit、--mode和--schedule之后再去研究单个规则开关。3. 环境准备获取、安装并验证 Vampire3.1 选择二进制包还是源码编译获取 Vampire 通常有两种方式从项目官网发布页下载预编译二进制包。从官方源码仓库克隆代码自己用 CMake 编译。预编译二进制包最快适合只想跑题目的场景。源码编译适合需要调试、修改源码或者需要在自己的服务器上复现比赛策略的场景。以官网实际发布为准不要假设某个版本号一定存在。下载后先执行--help和--version验证可执行文件是否正常工作。3.2 Linux 和 macOS 下启动下载解压后在终端中进入可执行文件所在目录./vampire --help ./vampire --version如果提示权限不足说明文件没有可执行权限chmod x vampire为了后续 Why3、Sledgehammer 等工具能自动发现 Vampire建议把可执行文件放到系统 PATH 中。例如复制到/usr/local/bin或者把安装目录加入 PATH。sudo cp vampire /usr/local/bin/ vampire --versionmacOS 上的做法类似。如果下载到的是 Darwin 平台二进制可以直接运行如果下载不到对应平台版本可以考虑源码编译。3.3 Windows 用户建议使用 WSLVampire 的许多比赛和验证脚本面向 Linux 环境。Windows 用户不建议直接在 cmd 或 PowerShell 里折腾二进制兼容性更推荐使用 WSL。在 WSL 中安装 Ubuntu 后按 Linux 方式下载或编译行为与真实 Linux 基本一致。这样可以避免很多路径分隔符、动态库和权限问题。3.4 源码编译示例如果选择源码编译通常需要git、cmake和g。在 Ubuntu/Debian 上可先安装基础工具sudo apt-get update sudo apt-get install -y git cmake g然后克隆源码并编译git clone 官方源码仓库地址 cd vampire cmake -B build -DCMAKE_BUILD_TYPERelease cmake --build build -j4编译完成后可执行文件通常位于build/bin目录下./build/bin/vampire --version源码编译需要的时间取决于机器配置。编译过程中的警告一般不影响使用但如果出现 CMake 版本过低或缺少依赖以构建日志为准。3.5 环境检查清单在进入具体题目之前可以按这个清单确认环境正常能执行vampire --version并输出版本信息。能执行vampire --help并看到可用参数。在当前目录下能读取.p文件。如果后续要接入 Why3确认vampire在 PATH 中。如果后续要在 Isabelle 中使用 Sledgehammer确认系统能找到可执行文件。这个清单很简单但能省掉后面排查“工具检测不到证明器”的大量时间。4. 最小可运行案例编写 TPTP 题目并完成第一次证明4.1 TPTP 格式的基础知识TPTP 是 Thousands of Problems for Theorem Provers 的缩写它既是题库格式也是定理证明器输入格式的事实标准。一个 TPTP 公式的基本结构是fof(名字, 角色, 公式).fof表示一阶公式名字必须唯一角色通常是axiom、hypothesis、conjecture或negated_conjecture。公式以句点结束。几点容易错的地方变量必须以大写字母开头常量、谓词和函数名以小写字母开头。注释用%到行尾或者用/* ... */。! [X] :表示全称量词? [X] :表示存在量词。连接词用、、~、、|。如果变量名写成小写Vampire 会把它当成一个常量语义完全改变。这是新手最常见的错误之一。4.2 案例一苏格拉底三段论创建文件socrates.p% 前提: 苏格拉底是人 fof(ax1, axiom, man(socrates)). % 前提: 所有人都会死 fof(ax2, axiom, ! [X] : (man(X) mortal(X))). % 目标: 苏格拉底会死 fof(conj, conjecture, mortal(socrates)).运行vampire socrates.p正常情况下输出中会出现Refutation found类似的字样。这说明 Vampire 先把目标取反与两个公理一起判断不可满足再推出矛盾。你也可以试试不改公式只把conjecture改成axiom然后在运行观察结果变化。这个练习有助于理解角色字段的作用。4.3 案例二等式的传递性Vampire 在带等式问题上的能力非常重要。创建eq_trans.pfof(ax1, axiom, a b). fof(ax2, axiom, b c). fof(conj, conjecture, a c).运行vampire eq_trans.p这个题目应该在很短时间内得到反证。如果没有得到检查是否用了中文标点、是否缺少句点或者文件名后缀是否被系统识别为.p。4.4 什么情况下输出不是 Refutation found如果输入的前提无法推出目标Vampire 不会输出Refutation found而可能输出Satisfiable或CounterSatisfiable等状态。举个例子fof(ax1, axiom, man(socrates)). fof(conj, conjecture, man(plato)).这个集合无法证明柏拉图是人。不同版本可能给出Satisfiable或CounterSatisfiable核心含义是存在一个解释让前提为真且目标为假所以目标不是必然定理。这一点很重要不要把GaveUp或Satisfiable理解为“结论肯定错了”。它们分别表示“没能找到证明”和“存在反例模型”。4.5 查看证明过程使用-p或--proof可以输出证明过程vampire --proof socrates.p输出中会列出经过变换和推理得到的子句以及最后推出空子句的步骤。初看可能觉得信息量大但这是理解反证过程最好的材料。建议在最小例子上看一次输出建立起“证明器做了什么”的直觉而不是只盯着最后一行状态。5. 参数、输出状态与结果解读5.1 常用命令行参数速查Vampire 参数很多建议先掌握下面这些参数作用示例--time_limit设置时间限制单位为秒--time_limit 30--memory_limit设置内存限制单位为 MB--memory_limit 4096--proof输出证明过程-p--input_syntax指定输入语法--input_syntax smtlib2--output_mode指定输出风格--output_mode tptp--mode选择运行模式--mode casc--schedule选择策略调度--schedule default--avatar控制 AVATAR 开关--avatar off不同版本的--mode、--schedule取值不一定相同实际使用前先看--help输出。这里提到的示例值用于说明参数形式不表示所有版本都支持相同的枚举值。5.2 输出状态的含义和判断Vampire 最终会返回一个状态根据输入是 “conjecture axioms” 还是 “纯公式集”状态含义略有差异。常见的状态如下输出状态含义对用户的意义Refutation found反证成功目标是定理Unsatisfiable公式集不可满足前提与目标否定矛盾Satisfiable公式集可满足存在解释使所有公式为真CounterSatisfiable存在反例模型目标不被前提支持GaveUp给定资源内未能判定不代表结论对错Timeout超过时间限制需要增大时间或换策略Memory limit exceeded超过内存限制需要减小子句规模或调整策略在使用自动定理证明器时最重要的是区分“证明不存在”和“没找到证明”。GaveUp只说明在当前参数和资源条件下没有找到不说明数学上目标不成立。5.3 时间和内存限制的意义实际验证中很少有人会无限期等待证明器运行。设置时间限制是防止单个目标拖垮整个流程的必要手段。vampire --time_limit 60 --memory_limit 8192 problem.p时间限制影响搜索深度内存限制影响子句保留数量。两者过小都会导致GaveUp但也不能无限增加。子句爆炸是自动定理证明的常见现象单纯加内存往往只是推迟问题而不是解决问题。5.4 自己构造可满足和不可满足的例子为了熟悉输出可以构造三组题目不可满足的例子公理和结论完全矛盾。可满足的例子前提不足目标只是可能成立。带等式的例子利用等式推理证明目标。依次运行并观察输出状态能很快建立对结果判读的信心。6. 在形式化验证工具链中接入 Vampire6.1 Why3 中的证明器配置Why3 是一个面向程序验证的通用平台它会把验证条件交给多种后端证明器。接入 Vampire 的常见步骤是先让 Why3 自动检测系统里的证明器why3 config detect检测通过后可以用why3 prove指定使用 Vampirewhy3 prove -P Vampire goal_file.mlw前提是vampire可执行文件位于 PATH 中。如果 Why3 检测不到优先检查 PATH而不是急着改 Why3 配置。6.2 Isabelle/HOL 中通过 Sledgehammer 调用在 Isabelle/HOL 中Sledgehammer 可以把当前目标交给多个外部证明器尝试。使用 Vampire 的方式是在命令中指定 proversledgehammer [provers vampire]Sledgehammer 会自动生成一个子问题并调用 Vampire 尝试证明。如果 Isabelle 检测不到 Vampire通常也是 PATH 问题或版本兼容问题。6.3 从高阶目标到一阶子目标Isabelle/HOL 默认逻辑是高阶逻辑而 Vampire 的核心是一阶逻辑。工具链在调用时通常会做翻译、抽象或类型化处理把可以被一阶证明的子目标拆分出来。因此不要期望 Vampire 能直接处理任意高阶逻辑定理。它能处理的是“翻译后的一阶子目标”。这也是为什么在集成工具链中Vampire 通常只承担一部分证明义务而不是替代整个交互式证明环境。6.4 在验证流程中的接入位置在实际工程流程中Vampire 常见的位置是作为 SMT 和交互式证明器的补充处理纯一阶逻辑但公式量大的目标。在回归测试中自动证明已经出现过的验证条件。在策略调度中与多个证明器并行多个工具互补。接入时要考虑输出解析、超时处理、日志记录和失败重试。生产环境的验证脚本不能只看返回码还要保存--proof输出作为证明证据。7. 常见问题与排查链路7.1 现象、原因和处理方式问题现象常见原因处理建议运行后提示找不到输入文件当前目录不对或文件名写错使用绝对路径或在正确目录运行提示没有权限下载的二进制未添加执行权限chmod x vampireTPTP 解析报错变量名小写、缺少句点、括号不匹配检查公式末尾句点变量大写一直输出GaveUp搜索空间过大、时间不足、策略不合适增加时间更换 schedule使用 SInE 筛选公理Why3 检测不到 Vampire不在 PATH 中确认vampire --version可用Isabelle Sledgehammer 报告 not found路径或版本兼容问题检查 PATH并查看 Isabelle 日志输出大量子句后内存耗尽子句爆炸限制内存切换到更积极化简的策略拆分问题7.2 从现象倒推问题的通用排查链路遇到任何异常按下面的顺序检查可以覆盖绝大多数情况输入文件是否存在路径是否正确。文件名后缀是否被正确识别必要时用--input_syntax显式指定。公式语法是否合法变量名大小写是否正确。每一个公式末尾是否有英文句点。是否把conjecture写成了axiom导致目标没有被取反。时间和内存限制是否过小。当前版本是否支持所用语法和参数。日志中是否出现具体的解析错误或断言信息。这个顺序适合学习阶段和生产环境调试。不要跳过前两步直接怀疑证明器本身。7.3 三个最常见的坑第一个坑是 TPTP 变量名写小写。! [x] :在 TPTP 中不是全称变量而是常量x。这会让量词语义完全改变甚至导致误判。第二个坑是把GaveUp当成结论错误。GaveUp只表示没有找到证明既不能说明目标成立也不能说明目标不成立。只有CounterSatisfiable才有反例语义。第三个坑是只验证了工具能启动没验证证明器能正常证明。很多集成问题是出在 PATH、版本、输入输出解析上而不是出在证明能力上。最小例子先跑通Refutation found再接真实目标。7.4 排查时如何缩小问题如果连最小例子都报错问题几乎一定在环境或格式上。此时不要说“工具不行”先做三步换一个官方文档或数据集中的标准 TPTP 例子。看完整错误输出而不要只看最后一行。用--help确认当前版本支持的参数名。如果最小例子能跑通只有大型问题失败那么问题更可能在证明策略、时间限制或资源消耗上。8. 最佳实践与学习路径8.1 学习路径清单从零开始掌握 Vampire建议按这个顺序理解一阶逻辑的语法和语义。理解反证法和不可满足性。跑通 TPTP 最小例子看懂Refutation found。试用--proof读一遍反证输出。学会看不同输出状态的区别。从 TPTP 题库中挑题目做批量测试。学习--time_limit、--memory_limit、--schedule等参数。了解 AVATAR 和 SInE 等高级机制。接入 Why3、Sledgehammer 等工具链。在真实验证任务中建立超时和失败处理机制。8.2 使用 Vampire 的工程建议在项目里使用 Vampire 时有几条建议可以直接落地。第一限制时间和内存不要无限运行。建议把超时时间设置为 30 到 60 秒内存限制根据机器配置设定避免一个目标拖垮整个验证流程。第二保存证明输出。当验证目标从失败变成成功时--proof输出可以作为回归依据。否则无法区分“换了参数后偶然成功”和“确实有稳定证明”。第三大型公理集优先考虑筛选机制。如果在几百条公理中证明一个目标直接全量输入会导致搜索空间爆炸。使用 SInE 或工具链提供的相关性选择只保留与目标相关的公理。第四不同问题可能适合不同策略。不要迷信某个参数在所有问题上都能赢。策略调度存在的意义正是用多组参数覆盖不同形态的问题。8.3 继续研究的方向Vampire 是一个研究性质很强的工具学习它并不只是为了跑通例子。深入方向可以从这里展开证明压缩看它是如何把长反证简化成短证明。策略生成理解不同参数组合对搜索空间的影响。与 SMT 的组合AVATAR 只用 SAT 做命题抽象后续还有更复杂的理论与一阶逻辑结合方向。在程序验证中的应用把循环不变式、前置条件和后置条件翻译成一阶目标后验证条件自动证明的工程化实现。对于刚入门的人来说最有价值的练习不是反复记参数而是把一个简单的数学定理翻译成 TPTP 格式再让 Vampire 证明它。这个过程会让你同时理解逻辑语义、格式规范和证明器行为比单纯读文档高效得多。