For any sentence $\alpha$, variable $v$, and constant symbol $k$ thatdoes NOT appear elsewhere in KB:$$\dfrac{\exists \nu. \alpha}{\mathsf{subst}(\{ \nu / k \},\alpha)}.$$E.g., $x. \mathrm{Crown}(x) \wedge \mathrm{OnHead}(x, \mathrm{John})$ yields$\mathrm{Crown}(C_1) \wedge \mathrm{OnHead}(C_1, \mathrm{John})$Provided $C_1$ is a new constant symbol (aka Skolemconstant)Can someone clarify the Skolem constant concept?
Skolem constant in existential instantiation for first order logic
artificial intelligence;first order logic