I have a set of closed formulas and i put them into clauses. I noticed that some of them are not horn clauses. For example i have:
not(S(x)) or L(x) or B(x)
Is it possible to apply the resolution principle using this clauses ?
ps: why in resolution principle we have to use the most general unifier ? Isn't a particular unifier sufficient ?