Let us go through each option:
1. Simplification: Make sentence simple eg: ~(~P)= P
2. Unification: Combine 2 sentences, replace variables with constants from each sentence, and simplify
- Sentence1: parents(x, father(x), mother(Bill))
- Sentence 2: parents(Bill, father(Bill), y)
- Unification Result: {x/Bill, y/mother(Bill)}
3. Skolemization : Removing all the existential quantifiers in a sentence with equivalent functions. Eg: (∃u) (∀v)P(f(u), v) is converted into (∀v)P(f(a), v)
4. Resolution: Deriving all possible combinations of given axiom and check whether they are true/false for goal statement. P|=Q
Answer of given question will be (C) Skolemization :