| 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
-
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)" -
Prenex Normal Form - Move all quantifiers to front - Standardize variables to avoid capture -
sympy_compute.py simplify "prenex(formula)" -
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
-
Resolution Proof - Convert to CNF, negate conclusion - Apply resolution rule until empty clause or saturation -
z3_solve.py prove "resolution_valid" -
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
uv run python -m runtime.harness scripts/z3_solve.py prove "ForAll([x], Implies(P(x), Q(x)))"
Z3_Exists
uv run python -m runtime.harness scripts/z3_solve.py sat "Exists([x], And(P(x), Not(Q(x))))"
Z3_Universal_Instantiation
uv run python -m runtime.harness scripts/z3_solve.py prove "Implies(ForAll([x], P(x)), P(a))"
Z3_Model
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.