论证验证器Skill argument-validator

---

name: argument-validator description: 此技能应用于当用户想要验证或批判一个论证时，通过提取前提、表面隐藏假设、检查逻辑有效性、可选的Lean形式化，以及研究前提支持。 license: MIT

论证验证器

概述

提供一个可重复的工作流程，用于将非正式论证转化为形式结构，识别关键假设，并通过可选的Lean形式化检查有效性和健全性。

何时使用

在用户要求以下操作时使用此技能：

• 验证或批判一个论证
• 在逻辑或Lean中形式化一个论证
• 识别隐藏假设或缺失前提
• 用反例测试论证
• 研究前提是否有证据支持

不要将此技能用于：

• 没有论证的简单意见问题
• 纯粹的风格重写
• 仅代码库的推理任务

工作流程

1. 澄清目标和范围

在形式化前询问缺失信息：

• 请求完整的论证文本、结论和预期受众
• 询问模糊术语的定义和论域
• 询问用户是否希望逻辑有效性、经验健全性，或两者兼有

2. 提取论证结构

将论证重述为编号列表：

• 将显式前提与隐式假设分开
• 将每个前提标记为逻辑的、定义的或经验的
• 注意任何模糊术语或范围变化

3. 形式化逻辑

转化为精确的形式表示：

• 选择适合的最小逻辑（命题逻辑或一阶逻辑）
• 明确定义符号和谓词
• 将论证编码为前提→结论
• 标记量词顺序和范围变化

4. 检查逻辑有效性

尝试从前提推导结论：

• 识别证明失败的第一个点
• 产生使有效性所需的最小额外假设
• 在可能时提供反例模型

5. 在Lean中形式化（可选）

当用户需要机器检查时，委托给Lean形式化器：

• 检查Lean可用性（lean --version 或 ~/.elan/bin/lean --version）
• 当没有项目时，使用 lean --stdin 进行快速检查
• 要求形式化器返回可编译的Lean代码片段以及缺失引理

6. 通过研究代理验证假设

对于每个经验性或可争议的假设：

• 每个假设生成一个研究子代理
• 提供确切的假设和所需的证据标准
• 要求提供摘要、来源和置信度评级
• 当有多个假设时，并行运行子代理

7. 合成最终分析

交付结构化摘要：

• 有效性判决（有效/无效）及理由
• 健全性判决（支持/不支持/未知）
• 关键假设列表及其证据状态
• 建议的修订以加强论证

子代理提示

形式化代理（逻辑 + Lean）

使用 general 子代理形式化论证：

您是形式化代理。

输入：
- 论证文本
- 提取的前提 + 结论
- 草案形式化（符号和公式）

任务：
1. 收紧形式化（最小逻辑）。
2. 识别缺失前提或隐式假设。
3. 尝试Lean形式化。
4. 如果证明失败，解释位置和原因。

输出：
- 精炼的形式化
- Lean定理陈述
- Lean证明草图或错误解释
- 缺失假设列表

假设研究代理

每个假设使用一个 general 子代理：

您是研究代理。

假设：
[插入假设]

任务：
1. 使用可用网络工具查找支持或反驳的来源。
2. 用引证摘要证据。
3. 评级置信度（低/中/高）。

输出：
- 证据摘要
- 来源列表及URL
- 置信度评级
- 冲突或缺口备注

输出格式

按此顺序提供结果：

1. 重述的论证（前提→结论）
2. 形式化（符号 + 公式）
3. 有效性分析（证明缺口或确认）
4. Lean检查结果（如果执行）
5. 假设表（前提、类型、证据、状态）
6. 解决不确定性的建议或问题