来源信息
- 仓库
- parcadei/Continuous-Claude-v3
- 最近来源活动
- 2026年1月10日 01:54
- 检测到的 SKILL.md 语言
- 英语
- 星标
- 3,943
- 分支
- 303
安装方式
默认使用会先检查来源的 Prompt；你也可以切换为直接命令，或下载本地副本。
检查来源文件
决定是否安装前，请先阅读 SKILL.md，以及 SkillsMP 当前展示的配套文件。
正在显示 SKILL.md
SKILL.md
来源说明 · 只读预览- name
- predicate-logic
- description
- Problem-solving strategies for predicate logic in mathematical logic
- allowed-tools
- ["Bash","Read"]
# Predicate Logic
## When to Use
Use this skill when working on predicate-logic problems in mathematical logic.
## Decision Tree
1. **Quantifier Analysis**
- Identify: ForAll (universal), Exists (existential)
- Scope of quantifiers and free/bound variables
- `z3_solve.py prove "ForAll([x], P(x)) implies P(a)"`
2. **Prenex Normal Form**
- Move all quantifiers to front
- Standardize variables to avoid capture
- `sympy_compute.py simplify "prenex(formula)"`
3. **Skolemization (for Exists)**
- Replace existential quantifiers with Skolem functions
- Exists x. P(x) -> P(c) or P(f(y)) depending on scope
- Needed for resolution-based proofs
4. **Resolution Proof**
- Convert to CNF, negate conclusion
- Apply resolution rule until empty clause or saturation
- `z3_solve.py prove "resolution_valid"`
5. **Model Theory**
- Construct countermodel to refute invalid argument
- Finite model for finite domain
- `z3_solve.py model "Exists([x], P(x) & Not(Q(x)))"`
## Tool Commands
### Z3_Forall
```bash
uv run python -m runtime.harness scripts/z3_solve.py prove "ForAll([x], Implies(P(x), Q(x)))"
```
### Z3_Exists
```bash
uv run python -m runtime.harness scripts/z3_solve.py sat "Exists([x], And(P(x), Not(Q(x))))"
```
### Z3_Universal_Instantiation
```bash
uv run python -m runtime.harness scripts/z3_solve.py prove "Implies(ForAll([x], P(x)), P(a))"
```
### Z3_Model
```bash
uv run python -m runtime.harness scripts/z3_solve.py model "Exists([x], P(x))"
```
## Cognitive Tools Reference
See `.claude/skills/math-mode/SKILL.md` for full tool documentation.
在 GitHub 查看