AtpMcp

AtpMcp

一个 MCP 服务，将 AtpClient 的四种定理证明器 后端——SystemOnTPTP、StarExec、Isabelle 和 LocalExec—— 作为工具提供给 Claude Code 和其他 MCP 宿主。

通过 stdio 使用 MCP 修订版 2026-07-28（JSON-RPC 2.0），且仅支持该 修订版：需要 initialize 握手（2025-11-25 及更早版本）的客户端会被拒绝。

使用 Docker 快速开始

镜像包含服务、Erlang 和 E prover，因此唯一的前提条件是 Docker。将服务添加到项目的 .mcp.json 中：

{
  "mcpServers": {
    "atp": {
      "command": "docker",
      "args": ["run", "-i", "--rm", "ghcr.io/jcschuster/atp_mcp:latest"]
    }
  }
}

这样即可使用 SystemOnTPTP（tptp.org 上的所有证明器）和本地 E（query_backend 中的 backend: "local_exec"），无需任何配置。

如需使用 Isabelle，请采用 latest-isabelle 标签（amd64，数 GB；容器需要数 GB RAM 来运行 HOL 会话）。服务会在首次调用 Isabelle 时启动 Isabelle 本身，这需要最多一分钟；同一会话中的后续调用会复用它。

要配置服务，请将项目挂载到 /work，它会在此处查找 atp_mcp.exs，并转发该文件读取的环境变量：

{
  "mcpServers": {
    "atp": {
      "command": "docker",
      "args": [
        "run",
        "-i",
        "--rm",
        "-v",
        "${PWD}:/work:ro",
        "-e",
        "STAREXEC_USER",
        "-e",
        "STAREXEC_PASS",
        "ghcr.io/jcschuster/atp_mcp:latest"
      ],
      "env": { "STAREXEC_USER": "me", "STAREXEC_PASS": "…" }
    }
  }
}

对于 Claude Code，还需在 .claude/settings.json 中批准该服务：

{
  "enabledMcpjsonServers": ["atp"]
}

要自行构建镜像：

docker build -t atp_mcp .                             # SystemOnTPTP + E
docker build -t atp_mcp:isabelle --target isabelle .  # + Isabelle/HOL

安装 escript

不使用 Docker 时，请安装 escript（Elixir 1.20 / OTP 29）：

mix escript.install hex atp_mcp
export PATH="$HOME/.mix/escripts:$PATH"

并在 .mcp.json 中使用 "command": "atp_mcp"。本地后端会使用 PATH 中的相应程序：local_exec 使用 eprover，Isabelle 后端使用 isabelle。

配置

escript 不会读取项目的 config/*.exs。它在启动时读取一个配置文件，按以下顺序选择第一个：

1. atp_mcp --config PATH；
2. ATP_MCP_CONFIG 环境变量；
3. 工作目录中的 atp_mcp.exs——对于 MCP 宿主来说，即项目根目录（容器中的 /work）。

该文件是普通的 Elixir Config，会在启动时执行，因此应从环境变量读取密钥，而不要将其写入文件：

# atp_mcp.exs
import Config

config :atp_client, :sotptp,
  default_system: "Vampire",       # a bare name runs the latest version
  default_time_limit_sec: 30

config :atp_client, :local_exec,
  binary: "vampire",
  args: ["--mode", "casc", "-t", "30"],
  cpu_timeout_s: 30

config :atp_client, :starexec,
  base_url: "https://starexec.example.org/starexec",
  username: System.get_env("STAREXEC_USER"),
  password: System.get_env("STAREXEC_PASS")

没有任何配置时：

• SystemOnTPTP 使用 tptp.org 和最新版本的 E。

• LocalExec 会在 PATH 中存在 eprover 时运行 eprover --auto --tstp-format --cpu-limit=30。

• Isabelle 会在 PATH 中存在 isabelle 时，于空闲端口启动名为 atp_mcp 的常驻服务，或复用已运行的服务。在容器外，该服务的运行时间会超过 MCP 进程，因此后续会话可跳过启动耗时。使用 isabelle server -n atp_mcp -x 停止它。若要使用自行运行的服务，请改为配置：

  config :atp_client, :isabelle,
    host: "isabelle.example.org",
    port: 9999,
    password: System.get_env("ISABELLE_PASSWORD")
  

  并设置 config :atp_mcp, isabelle_autostart: false，以排除本地服务。

• StarExec 没有默认值；它需要 base_url、username 和 password。

所有设置请参阅 AtpClient 文档。

检查设置

atp_mcp doctor 会针对每个后端输出解析出的设置以及该后端是否可访问。请按 MCP 宿主启动服务的方式运行它：

$ docker run --rm -v "$PWD:/work:ro" ghcr.io/jcschuster/atp_mcp doctor
atp_mcp 0.8.0
config file: /work/atp_mcp.exs

sotptp - SystemOnTPTP
  url: "https://tptp.org/cgi-bin/SystemOnTPTPFormReply"
  default_system: "Vampire"
  default_time_limit_sec: 30
  check: OK
…

指定后端名称即可只检查这些后端（atp_mcp doctor sotptp local_exec）。任何检查失败时，程序都会以状态码 1 退出；密码仅显示为已设置或未设置。

工具

跨后端（统一的 AtpClient.Backend）

list_backends

列出服务提供的所有后端（sotptp、isabelle、local_exec、starexec）及其易读标签。

describe_szs

返回 SZS Ontology 的文本参考资料——每个证明器判定结果都使用其中的词汇。列出所有 Success 状态（Theorem、Unsatisfiable、Satisfiable、CounterSatisfiable、ContradictoryAxioms，……）和 NoSuccess 状态（GaveUp、Timeout、ResourceOut、MemoryOut、Forced、InputError，……），并附上其助记符和定义，让 Agent 无需离开 MCP 会话即可判断判定结果的含义。内容根据 Tptp.Szs.Ontology 生成，该表正是依据它解读判定结果。不接受参数。

verify_backend

探测后端的配置和可达性。返回 OK 或描述性错误。

参数	类型	必填	说明
backend	string	是	sotptp | isabelle | local_exec | starexec

后端专属的覆盖键（base_url、password、binary，……）会透传给后端的 verify/1。

query_backend

通过统一的 c:AtpClient.Backend.query/2 入口向任意后端提交 TPTP 格式的问题，并返回 SZS Ontology 判定结果（Theorem、Unsatisfiable、Satisfiable、CounterSatisfiable、GaveUp、Timeout、ResourceOut，……）。完整词汇表请调用 describe_szs。

参数	类型	必填	说明
backend	string	是	sotptp | isabelle | local_exec | starexec
problem	string	是	TPTP 问题文本
time_limit_sec	integer	否	由支持该参数的后端应用（sotptp）
raw	boolean	否	返回系统未经修改的输出，而非 SZS 判定结果

每个后端的覆盖参数都会透传（例如，local_exec 的 binary、isabelle 的 timeout_ms、starexec 的 base_url，以及 system——即 local_exec 二进制文件或 starexec 求解器所用证明器在 SystemOnTPTP 中的名称，用于读取其输出）。

SystemOnTPTP

list_provers

列出 SystemOnTPTP 上所有可用的定理证明器系统。

run_prover

向指定证明器提交 TPTP 问题，并返回其 SZS 状态。

参数	类型	必填	说明
problem	string	是	TPTP 问题文本
system_id	string	是	来自 list_provers 的证明器 ID，或不带版本号的名称（如 Vampire），表示最新版本
time_limit_sec	integer	否	时间限制，单位为秒
raw	boolean	否	返回证明器未经修改的输出，而非 SZS 判定结果

compare_provers

同时使用多个证明器运行同一个问题，并并排返回所有结果，每个请求的系统对应一行，顺序与给定顺序一致。不带版本号的名称会显示所运行的版本：

Vampire (Vampire---5.0.1): CounterSatisfiable
E---3.5.1: CounterSatisfiable
Nope: not a system on SystemOnTPTP (see list_provers)

参数	类型	必填	说明
problem	string	是	TPTP 问题文本
system_ids	string[]	是	要比较的证明器 ID 或不带版本号的名称
time_limit_sec	integer	否	每个证明器的时间限制，单位为秒

Isabelle

prove_isabelle

将手写的 Isabelle/HOL 理论提交到已配置的 Isabelle 服务。理论文本会写入已配置的共享目录，并通过 use_theories 处理。对于 TPTP/THF 问题，请改用 query_backend，并设置 backend: "isabelle" — 这会通过 prove_tptp 进行路由。会话、主机、端口和密码仅从配置中读取。

参数	类型	必填	描述
theory	string	是	Isabelle 理论文本（完整内容或仅正文）
theory_name	string	是	理论名称（也用作 .thy 文件名）
timeout_ms	integer	否	use_theories 的整体超时时间，单位为毫秒
raw	boolean	否	返回 Isabelle 的消息文本，而非判定结果

诊断

lint_problem

对 TPTP 问题执行语法和类型诊断。默认将进程内的 tptp 检查器（Tptp.analyze/2） 与 SystemOnTPTP 上的 TPTP4X 结合使用；传入 backends: ["local"] 则仅执行开销较低的检查。 如果本地检查已发现错误，则跳过 TPTP4X。每项发现按 line:column [severity] (source) message [code] 的格式报告， 并附上检查器提供的提示（如果有），随后列出已声明的符号及其类型：

2:8 [warning] (tptp) "axim" is not a TPTP formula role [TPTP0401]
    hint: expected one of axiom, hypothesis, definition, …
2:12 [error] (tptp4x) Invalid role, exiting [TPTP4X]

Symbols:
  plus : $i > $i (declared at 1:14)

参数	类型	必填	描述
problem	string	是	TPTP 问题文本
backends	string[]	否	["local", "tptp4x"] 的子集；默认运行两者

示例

MCP 服务启动后，你可以向 Claude Code 提出如下问题：

“SystemOnTPTP 上哪些证明器可以证明这个 TPTP 问题？比较 Vampire、E 和 Satallax。”

Claude 将直接调用 compare_provers 并报告 SZS 结果。

“用我本地的 E 版本运行这个问题，然后在 SystemOnTPTP 上进行合理性检查。”

Claude 将调用两次 query_backend — 一次设置 backend: "local_exec"， 一次设置 backend: "sotptp" — 并比较判定结果。

Agent 技能

skills/atp-mcp/SKILL.md 是一种 Agent 技能，旨在教会 Agent 使用这些 工具：TPTP 方言及接受这些方言的证明器、先检查再证明的 工作流，以及每种 SZS 判定结果可以得出什么结论。它还列出了证明器可以提供帮助的任务， 例如自动形式化、检查证明和寻找反例，让 Agent 无需提示便会主动使用这些工具。要在 Claude Code 中使用，请将该目录复制到项目中的 .claude/skills/ 或 ~/.claude/skills/。

取消与进度

长时间运行的工具调用在各自的 Task 中执行。MCP 主机可以：

• 发送带有正在执行的请求 ID 的 notifications/cancelled，以中止 调用。调用方终止时，每个 AtpClient 后端都会清理其上游任务：

  • LocalExec 通过关闭 Port，向证明器二进制发送 SIGKILL。
  • StarExec 对远程任务发出 DELETE 请求。
  • Isabelle 断开会话，从而中止服务端正在执行的 use_theories 任务。
  • SystemOnTPTP 关闭本地连接，但远程证明器会继续运行，直到达到其 :time_limit_sec — SOTPTP 没有远程取消接口。

• 在 tools/call 上设置 _meta.progressToken，即可在调用执行期间接收定期的 notifications/progress 帧。默认每五秒发送一次心跳；可通过以下方式覆盖：

  config :atp_mcp, heartbeat_ms: 10_000
  

前言：MCP Tasks 扩展

MCP Tasks（立即调用，稍后通过任务句柄获取结果）与 ATP 工作流几乎完全契合。修订版 2026-07-28 将它们从核心协议移至官方扩展 io.modelcontextprotocol/tasks。MCP 宿主支持该扩展后，这里的长时间运行工具就应返回任务，这也会让类似 StarExec 的 submit_job / await_job 配对变得顺理成章。

许可证

MIT。