用途
该技能用于处理数理逻辑中的证明论（proof theory）问题。当需要构造、分析或验证形式化证明时，可参考其提供的策略与工具命令。
主要能力
证明策略选择
提供决策树式的策略选择：
- 直接证明：假设前提，推导结论
- 反证法：假设否定，推导出假
- 分情况证明：按析取式拆分
- 归纳法：基例加归纳步
结构归纳
- 在结构上定义良基序
- 基例：对最小元素证明
- 归纳步：假设较小元素成立，证明当前元素成立
对应命令：
z3_solve.py prove "induction_principle"
切消
- Gentzen 主定理（Hauptsatz）：切可被消除
- 子公式性质：只出现子公式
- 用于证明规范化
可靠性与完备性检查
- 可靠性：若可证明则有效
- 完备性：若有效则可证明
对应命令：
z3_solve.py prove "soundness_theorem"
证明验证
- 检查每一步是否由规则推出
- 验证依赖是否满足
对应命令：
math_scratchpad.py verify "proof_steps"
使用方式
通过以下工具命令调用：
归纳基例：
uv run python -m runtime.harness scripts/cc_math/z3_solve.py prove "P(0)"
归纳步：
uv run python -m runtime.harness scripts/cc_math/z3_solve.py prove "ForAll([n], Implies(P(n), P(n+1)))"
可靠性：
uv run python -m runtime.harness scripts/cc_math/z3_solve.py prove "Implies(derivable(phi), valid(phi))"
数学验证：
uv run python -m runtime.harness scripts/cc_math/math_scratchpad.py verify "proof_structure"
完整工具文档参见 .claude/skills/math-mode/SKILL.md。
适用场景
适用于数理逻辑中证明论相关任务，包括证明策略选择、结构归纳、切消分析、可靠性与完备性检查以及证明步骤验证。
限制
资料未提供该技能的具体实现细节、依赖环境版本、支持范围边界或性能说明，暂未提供。