用途：该技能用于处理数学逻辑中的谓词逻辑问题，提供一套问题求解策略与配套工具命令。
主要能力：涵盖量词分析（识别全称量词 ForAll 与存在量词 Exists，分析量词辖域及自由/约束变量）、前束范式（将量词前移并标准化变量以避免捕获）、Skolem 化（用 Skolem 函数替换存在量词，服务于基于归结的证明）、归结证明（转换为 CNF、否定结论、反复应用归结规则直至空子句或饱和）、模型论（构造反模型以反驳无效论证，有限域用有限模型）。
使用方式：通过命令行调用脚本，例如 uv run python -m runtime.harness scripts/z3_solve.py prove "ForAll([x], Implies(P(x), Q(x)))"、uv run python -m runtime.harness scripts/z3_solve.py sat "Exists([x], And(P(x), Not(Q(x))))"、uv run python -m runtime.harness scripts/z3_solve.py model "Exists([x], P(x))"，以及 sympy_compute.py simplify "prenex(formula)"。完整工具文档见 .claude/skills/math-mode/SKILL.md。
适用场景：谓词逻辑证明、有效性判定、反模型构造等数学逻辑任务。
限制：资料未提供具体安装步骤、依赖版本、收费信息或性能说明，相关细节暂未提供。