We are in first order logic and I have 2 formulas and a logical consequence:
$$u(s),\forall x(u(x) \rightarrow m(x)) \models m(s)$$
and I want to prove it using semantic resolution. (it's a didactical exercise).
I have two questions:
- Do I have to define a domain before proceeding to the semantic resolution?
- In this case, is it possible to enumerate every possible case? When is it not possible?