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