用途：该技能用于处理数学逻辑中的命题逻辑问题，帮助判断公式性质并完成推理验证。
主要能力：提供决策树式流程，先识别公式结构，判断是重言式、矛盾式还是偶然式，并识别主联结词（AND、OR、IMPLIES、NOT、IFF）。支持真值表方法，适用于变量数不超过 4 的小公式，通过枚举所有赋值判断：全为真即重言式，全为假即矛盾式。支持自然演绎，应用肯定前件、否定后件等推理规则，以及条件证明（假设前件推导后件）。还支持语义表方法，通过分解公式构建树，封闭分支表示矛盾，所有分支封闭则论证有效。
使用方式：可用 z3_solve.py 检查可满足性，例如 uv run python -m runtime.harness scripts/z3_solve.py sat "And(p, Implies(p, q), Not(q))"；证明重言式或肯定前件，例如 uv run python -m runtime.harness scripts/z3_solve.py prove "Implies(And(p, Implies(p,q)), q)"；用 sympy_compute.py 生成真值表，例如 uv run python -m runtime.harness scripts/sympy_compute.py truthtable "p & (p >> q) >> q"。
适用场景：命题逻辑公式性质判定、可满足性检查、推理有效性验证与教学演示。
限制：真值表方法仅适合小规模公式；完整工具文档见 .claude/skills/math-mode/SKILL.md。其他细节暂未提供。