predicate-logic
Scannednpx machina-cli add skill parcadei/Continuous-Claude-v3/predicate-logic --openclawPredicate 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.
Source
git clone https://github.com/parcadei/Continuous-Claude-v3/blob/main/.claude/skills/math/mathematical-logic/predicate-logic/SKILL.mdView on GitHub Overview
This skill provides practical strategies for solving predicate-logic problems in mathematical logic, guiding you through quantifier analysis, prenex normalization, Skolemization, resolution proofs, and model-theory checks. It also demonstrates how to apply these steps using command-line tools to automate reasoning.
How This Skill Works
You start by analyzing quantifiers and the scope of variables, then move the formula to prenex normal form with standardized variables. For existentials, Skolemization replaces them with functions to enable resolution. Convert to CNF and perform resolution, or construct countermodels via model theory when needed. The process is illustrated with tool commands such as z3_solve.py prove/sat/model together with example formulas.
When to Use It
- When you need to analyze the scope of universal and existential quantifiers in a predicate-logic problem.
- When converting a formula to prenex normal form and avoiding variable capture during standardization.
- When applying Skolemization to existential quantifiers to enable resolution-based proofs.
- When performing CNF conversion and a resolution-based proof to establish validity or satisfiability.
- When you want to construct countermodels using model theory to refute invalid arguments.
Quick Start
- Step 1: Identify quantifiers and their scopes in your formula.
- Step 2: Move quantifiers to the front (prenex) and apply Skolemization if needed.
- Step 3: Convert to CNF and attempt a resolution proof or construct a countermodel.
Best Practices
- Identify quantifiers and carefully track free vs. bound variables.
- Standardize variable names to prevent capture during prenexing.
- Apply Skolemization correctly to preserve satisfiability in existential quantifiers.
- Convert formulas to CNF and negate the conclusion for a resolution proof.
- Use model-theory checks to build countermodels when resolution fails.
Example Use Cases
- Prove: ForAll([x], Implies(P(x), Q(x))).
- Check satisfiability: Exists([x], And(P(x), Not(Q(x)))).
- Instantiate universal: Implies(ForAll([x], P(x)), P(a)).
- Model question: Exists([x], P(x)).
- Resolution workflow: Convert to CNF and apply resolution to derive an empty clause.
