I have been spending some time studying the HORN algorithm, but my textbook, as well as most posts online, are quite vague around the steps taken.
These are the steps from my textbook:
My questions:
- For step 1, when marking T, should you also mark the conclusion if T is the premise? For example, if you have T → p, should you mark both T and p in your first step?
- When going through the remaining "loop" of marking the atoms, how do you know in which order to mark the atoms?
The actual problem I am looking at is as follows:
(p ∧ q ∧ s → p) ∧ (q ∧ r → p) ∧ (p ∧ s → s) ∧ (T → r)
So, my assumption is that the steps will go as follows:
STEP 1: (p ∧ q ∧ s → p) ∧ (q ∧ r → p) ∧ (p ∧ s → s) ∧ (T → r)
STEP 2: (p ∧ q ∧ s → p) ∧ (q ∧ r → p) ∧ (p ∧ s → s) ∧ (T → r)
Looking at my steps, I am marking p as the next atom, but I am not sure why - it could also be q, s or r.
Any clarity on this would be greatly appreciated!
Thanks
(1) There's presumably more to the algorithm than you've given here. Specifically, "that list" in step 1 should be preceded by something saying what list is meant.
(2) If you mark $\top$ in step 1 and $\top$ is the premise of some clause, then it wouldn't hurt to also mark the conclusion, but if you strictly follow the specified steps then you'd mark that conclusion in an instance of step 2 with $k_i=0$ (because $\top$ is the conjunction of $0$ conjuncts).
(3) Something's wrong in step 2 of your example. Why have you marked $p$? The algorithm allows you to mark $r$ but nothing else.
(4) In your example, running the algorithm seems a waste of time. Since there's no $\bot$ in your formula, there's no way the algorithm could produce the output "The Horn formula $\phi$ is unsatisfiable". Indeed, your formula is obviously satisfiable by giving all the variables the value "true".