Skolemization

The Weak GDV Way

• Try prove I_Sk from I_Ax
  • Almost inevitably fails
• Prove I_Ax from I_Sk
  • Typically succeeds
  • Incomplete verification, but catches stupid mistakes

The Principled Way

• Generate an ε-term for the Skolem symbol
  • Will ATP system developers do that?
• Prove I_Sk from { I_Ax, ε_Sk }
  • It can be done
  • ε-term provides meaning, e.g., looking at proofs
  • Relies on a meta-argument

The Pragmatic Way

• Use a trusted Skolemizer to generate a trusted Skolemization T_Sk
  • Skolemize same variable, same symbol,
  • It can be (is being!) done
• Prove I_Sk from T_Sk
  • Likely to succeed
  • Vulnerable to optimizations