Let's say that we have the following formulas:
φ = ∃x∀y(A(x,y))
β = A(a,b)
where x,y are variables, A is a predicate and a,b are constants.
Now if I convert φ into an equisatisfiable clause, I will end up with
φ' = ∀y(A(sk1,y))
where sk1 is a new Skolem's constant.
Now if I were to apply unification to φ' and β (to find their resolvents, for example), I would have to look for a valid substitution for both formulas.
Substituting y / b is clear. But what about sk1 and a? These are two constants that aren't equal, so if the algorithm were to be applied here, it would output "substitution not possible". But now that I'm thinking about it, isn't there a chance that these two constants will be the same?
Should Skolem's constants be considered equal to any other constant that we compare it to? Or should I simply follow the unification algorithm without differentiating between Skolem's constants and normal non-Skolem constants (therefore outputting "no valid substitution possible").
Thank you in advance.
The two constants don't have the same name, but that doesn't prevent them being assigned the same value in an interpretation. The terms $ski$ and $a$ don't have a unifier, but that doesn't affect the completeness of resolution theorem proving. Resolution theorem-proving works by trying to instantiate variables in a set of first-order formulas until a contradiction is found. That contradiction will apply to any assignment of values to the constants, including assignments that map two or more constants with different names to the same value.