Existential instantiation (El) For any sentence a,variable v,and constant symbol k that does not appear elsewhere in the knowledge base: 3va Subst({v/k},a) E.g.,3x Crown(x)^OnHead(x,John)yields: Crown(C1)OnHead(C1,John) provided C,is a new constant symbol,called aExistential instantiation (EI) • For any sentence α, variable v, and constant symbol k that does not appear elsewhere in the knowledge base: • v α Subst({v/k}, α) • E.g., x Crown(x)  OnHead(x,John) yields: Crown(C1 )  OnHead(C1 ,John) provided C1 is a new constant symbol, called a Skolem constant