跳到主要内容
知仓学习社ZHICANG

proof-theory

Problem-solving strategies for proof theory in mathematical logic

不碰外部(只输出文字)无严重或高危命中parcadei/Continuous-Claude-v3

它会碰到什么

扫了多少1 个文本文件,2 KB
它会碰到什么不碰外部(只输出文字)
命中总数0 处
命中统计严重 0 · 高 0 · 中 0 · 低 0

这一栏是扫描器报的事实,不是结论。命中多不等于有毒(安全工具、规则库、示例脚本本来就会包含危险写法),命中少也不等于干净。它和你手上的凭据、文件、网络有什么关系,需要你自己看。

技能内容

Proof Theory

When to Use

Use this skill when working on proof-theory problems in mathematical logic.

Decision Tree

  1. Proof Strategy Selection
  • Direct proof: assume premises, derive conclusion
  • Proof by contradiction: assume negation, derive false
  • Proof by cases: split on disjunction
  • Induction: base case + inductive step
  1. Structural Induction
  • Define well-founded ordering on structures
  • Base: prove for minimal elements
  • Step: assume for smaller, prove for current
  • z3_solve.py prove "induction_principle"
  1. Cut Elimination
  • Gentzen's Hauptsatz: cuts can be eliminated
  • Subformula property: only subformulas appear
  • Useful for proof normalization
  1. Completeness/Soundness Check
  • Soundness: if provable then valid
  • Completeness: if valid then provable
  • z3_solve.py prove "soundness_theorem"
  1. Proof Verification
  • Check each step follows from rules
  • Verify dependencies are satisfied
  • math_scratchpad.py verify "proof_steps"

Tool Commands

Z3_Induction_Base

uv run python -m runtime.harness scripts/cc_math/z3_solve.py prove "P(0)"

Z3_Induction_Step

uv run python -m runtime.harness scripts/cc_math/z3_solve.py prove "ForAll([n], Implies(P(n), P(n+1)))"

Z3_Soundness

uv run python -m runtime.harness scripts/cc_math/z3_solve.py prove "Implies(derivable(phi), valid(phi))"

Math_Verify

uv run python -m runtime.harness scripts/cc_math/math_scratchpad.py verify "proof_structure"

Cognitive Tools Reference

See .claude/skills/math-mode/SKILL.md for full tool documentation.

想直接用这个技能?

本站把开放许可(MIT / Apache 等)的技能按仓库打包整理到网盘,点一下转存到你自己的网盘,不用一个个从 GitHub 拉。许可未声明的技能只给原始仓库链接,不打包。