I'm trying to apply resolution to this term to proof if α |= β is valid.
α = (¬ A ∨ B) ∧ (A ∨ B ∨ ¬ D) ∧ (¬ B ∨ (A ∧ ¬ D)) ∧ (¬ A ∨ ¬ B ∨ D)
β = A → D
I used the distributive property to convert the partial formula (¬ B ∨ (A ∧ ¬ D)) into (¬ B ∨ A) ∧ (¬ B ∨ ¬ D). So the current version looks like this:
α = (¬ A ∨ B) ∧ (A ∨ B ∨ ¬ D) ∧ (¬ B ∨ A) ∧ (¬ B ∨ ¬ D) ∧ (¬ A ∨ ¬ B ∨ D)
The resolution gives me different results. Sometimes I get ¬ B sometimes ¬ D and sometimes ¬ D ∨ ¬ C. Depending on the order in which I clear the atoms (is that normal?). In the other exercises, the empty set always came out at the end, or you had a clear result. I don't think I understand the problem correctly either, since we have always used the resolution to check whether the formula can be satisfied at all, i.e. whether an empty set results or not.
Thanks in advance for any tip!
