I'm a little bit lost when it comes to Horn formulas. What exactly do they mean by "marking"? Could someone maybe provide a simple example of how to apply the HORN algorithm to a Horn formula so I can see it in action?
Marking it means exactly that. Write out the formula, in full on paper, and when the algorithm tells you to mark a clause, do so either by placing a tick above that clause, or underlining it, or highlighting, you get the idea.
For example, take the formula (p2 ^ p3 ^ p5 -> p13) ^ (T -> p5) ^ (p5 ^ p11 -> _). T stands for tautology, and _ for contradiction, else have a look at the third equation on page 66 if my symbology makes no sense to you.
Right, step 1 says mark all T's, so after this step, our equations looks as follows:
Where does the book say it's unsatisfiable? I'm looking on pg 66. The first three equations are Horm formulas, the following four are not.
1. It marks if it occurs in that list.
2. If there is a conjunct P1 Ã¢Ë†Â§ P2 Ã¢Ë†Â§ Ã‚Â· Ã‚Â· Ã‚Â· Ã¢Ë†Â§ Pki Ã¢â€ â€™ P of Ãâ€ such that all Pj with 1 Ã¢â€°Â¤ j Ã¢â€°Â¤ ki are marked, mark P as well and go to 2. Otherwise (= there is no conjunct
P1 Ã¢Ë†Â§ P2 Ã¢Ë†Â§ Ã‚Â· Ã‚Â· Ã‚Â· Ã¢Ë†Â§ Pki Ã¢â€ â€™ P such that all Pj are marked) go to 3.
3. If Ã¢Å Â¥ is marked, print out Ã¢â‚¬ËœThe Horn formula Ãâ€ is unsatisfiable.Ã¢â‚¬â„¢ and stop. Otherwise,
go to 4.
4. Print out Ã¢â‚¬ËœThe Horn formula Ãâ€ is satisfiable.Ã¢â‚¬â„¢ and stop.
Step 3 says if Ã¢Å Â¥ is marked (which in our example it isn't), print unsatisifiable Otherwise goto 4. So, we go to 4
Step 4 says: Satisfiable
sorry, i'm looking at number 3 of the four wrong formulas. i thougth ur example was based on that one. thanks.
on top, can u clear the explanation why p13 Ã¢Ë†Â§ p27 is not type of P (on the 3rd fomula of the 4 examples of "not Horn formulas".