Welcome! Log In Create A New Profile

# Horn Formula

Posted by Moonfruit
Announcements Last Post SoC Curricula 09/30/2017 01:08PM Demarcation or scoping of examinations and assessment 02/13/2017 07:59AM School of Computing Short Learning Programmes 11/24/2014 08:37AM Unisa contact information 07/28/2011 01:28PM
 Horn Formula March 18, 2008 03:37PM Registered: 12 years ago Posts: 18 Rating: 0
Hi there

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?

Thanks
Justin
 Re: Horn Formula March 21, 2008 03:51PM Registered: 13 years ago Posts: 39 Rating: 0
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:

(p2 ^ p3 ^ p5 -> p13) ^ (T -> p5) ^ (p5 ^ p11 -> _)

Step 2 says (in essence) that if everything on the left-hand side of -> is marked, then mark the right-hand side too.

So, now our formula look like this

(p2 ^ p3 ^ p5 -> p13) ^ (T -> p5) ^ (p5 ^ p11 -> _)

Reading the fine print under the description of the algorithm in the book ,we see that if you mark p5 in one place, then ALL p5's must be marked. So:

(p2 ^ p3 ^ p5 -> p13) ^ (T -> p5) ^ (p5 ^ p11 -> _)

Step 3 says as soon as step 2 can no longer be repeated (and if no _'s are marked), move to step 4.

In step 4, _ is not marked, so we exit the algorithm as satisfiable. If p11 was marked though, then we would have had an unsatisfiable formula.

There you go! This is how I interpret it. If I'm wrong, hopefully someone else will point out my misunderstanding, else I hope this helps you...

Now, you can kindly return the favour and help me out on my query, which I'll post in the next 5 minutes Re: Horn Formula April 25, 2008 09:22AM Registered: 14 years ago Posts: 88 Rating: 0
hey guys, sorry for posting so late, just got the book last week, on ur explanation, how does line 3 on the same page returns 'unsatisfiable'?
 Re: Horn Formula April 25, 2008 09:32AM Registered: 13 years ago Posts: 39 Rating: 0
Que? Sorry, giggs, please rephrase that question. I have no idea what you're asking.
 Re: Horn Formula April 25, 2008 10:18AM Registered: 14 years ago Posts: 88 Rating: 0
sorry,
u wrote "In step 4, _ is not marked, so we exit the algorithm as satisfiable. If p11 was marked though, then we would have had an unsatisfiable formula."

according to what i've marked, p11 was not marked, then we have satisfiable formula, so my quetion is, how come the book says we have unsatisfiable formula?
 Re: Horn Formula April 25, 2008 10:43AM Registered: 13 years ago Posts: 39 Rating: 0
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.

THe algorithm...

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

Am I missing something?
 Re: Horn Formula April 25, 2008 11:09AM Registered: 14 years ago Posts: 88 Rating: 0
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" .
Sorry, only registered users may post in this forum.

Click here to login