⚡

谓词逻辑Skill predicate-logic

这个技能专注于数学逻辑中的谓词逻辑问题解决，提供量词分析、前束范式转换、斯科伦化、消解证明和模型理论等策略。适用于逻辑推理、证明验证和形式化方法。关键词：谓词逻辑，数学逻辑，问题解决，Z3求解器，逻辑证明，形式验证。

数据分析 0 次安装 0 次浏览 更新于 3/14/2026

name: 谓词逻辑 description: “数学逻辑中谓词逻辑的问题解决策略” allowed-tools: [Bash, Read]

谓词逻辑

使用时机

在数学逻辑中处理谓词逻辑问题时使用此技能。

决策树

  1. 量词分析

    • 识别：全称量词 (ForAll)，存在量词 (Exists)
    • 量词的作用域和自由/绑定变量
    • z3_solve.py prove "ForAll([x], P(x)) implies P(a)"

  2. 前束范式

    • 将所有量词移到前面
    • 标准化变量以避免捕获
    • sympy_compute.py simplify "prenex(formula)"

  3. 斯科伦化 (对于存在量词)

    • 用斯科伦函数替换存在量词
    • Exists x. P(x) -> P© 或 P(f(y))，取决于作用域
    • 用于基于消解的证明

  4. 消解证明

    • 转换为合取范式，否定结论
    • 应用消解规则直到空子句或饱和
    • z3_solve.py prove "resolution_valid"

  5. 模型理论

    • 构建反模型来反驳无效论证
    • 有限域的有限模型
    • z3_solve.py model "Exists([x], P(x) & Not(Q(x)))"

工具命令

Z3_全称量词

uv run python -m runtime.harness scripts/z3_solve.py prove "ForAll([x], Implies(P(x), Q(x)))"

Z3_存在量词

uv run python -m runtime.harness scripts/z3_solve.py sat "Exists([x], And(P(x), Not(Q(x))))"

Z3_全称实例化

uv run python -m runtime.harness scripts/z3_solve.py prove "Implies(ForAll([x], P(x)), P(a))"

Z3_模型

uv run python -m runtime.harness scripts/z3_solve.py model "Exists([x], P(x))"

认知工具参考

查看 .claude/skills/math-mode/SKILL.md 获取完整的工具文档。