Welcome! Log In Create A New Profile

Advanced

Horn Formula

Posted by Moonfruit 
Announcements Last Post
Announcement SoC Curricula 09/30/2017 01:08PM
Announcement Demarcation or scoping of examinations and assessment 02/13/2017 07:59AM
Announcement School of Computing Short Learning Programmes 11/24/2014 08:37AM
Announcement Unisa contact information 07/28/2011 01:28PM
Horn Formula
March 18, 2008 03:37PM
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
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 smiling smiley
Re: Horn Formula
April 25, 2008 09:22AM
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
Que? Sorry, giggs, please rephrase that question. I have no idea what you're asking.
Re: Horn Formula
April 25, 2008 10:18AM
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
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
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"winking smiley.
Sorry, only registered users may post in this forum.

Click here to login