horn clause lisp

Hi Everybody,
I'm new on this forum,
i'm trying to develop a lisp application that return T if a clause is a horn clause http://en.wikipedia.org/wiki/Horn_clause (or conjunction of horn clauses) and nil if it isn't.
I wont to clarify that in case of conjunction of horn clauses, the conjucntion could be between * clauses (from 0 to infinite).
I post you the code i've writtent till now that doesn't works and some examples that shloud be verified but (till now they don't) ...maybe somebody could help me to fix it... thank's everybody

(defun hornp-helper (fbf)
(cond ((or (not (equal 'not (first fbf))) (not (equal 'or (first fbf)))) (horn-positive (rest fbf)))
      ((equal 'not  (first fbf)) (hornp-helper (rest fbf)))
      ((equal 'and (first fbf)) (horn-positive (rest (rest fbf))))
      ((null fbf) T)))

(defun horn-positive (fbf)
(cond ((null fbf) T)
      ((equal 'not (first fbf)) (horn-positive (rest (rest fbf))))
      ((not (equal 'not (first fbf))) nil)
      
))



	
(defun hornp (fbf)
(cond ((equal '==> (first fbf)) (hornp-helper (rest fbf)))
       ))
         

CL-USER> (hornp ’(==> p (or q w)))
NIL

CL-USER>(hornp ’(==> (and p q) r))
T

CL-USER>(hornp ’(==> p (not q))
T

Hi zen34,

As someone who knows some maths, but not logic, for me the Wikipedia article about Horn Clauses is very difficult to understand . If you could explain what a Horn Clause is using simpler language (or maybe an "Introduction to ..." page), I could help more (others would probably find it easier too). If you can do that, you might figure out what the problem is without our help .

Having said that, don't let me stop anyone else answering this .

P.S. Please use a spell checker (for example, visit this web page using Mozilla Firefox).

The OP question is better asked here http://informatica.elearning.unimib.it. And the answer is really in the slides and in the project handout. But then again, time is almost up , so whatever will be handed in will be evaluated on its own merit

Marco Antoniotti

I think the easier way to do this is to expand the clause in a disjunction of literals.

In an implication, the precedent should be a literal clause or it should be a conjunction of clauses (or maybe expandable to a conjunction of clauses, it depends on the application, or how your teacher defined the problem). The consequent of the implication should be a disjunction of clauses or a single clauses. To expand this implication in a conjunction of literals, you join the negation of literals of the conjunction of the precedent and the disjunction of literals of the consequent.

For instance,

'(==> (and a (not b) c) (or d (not e) f))

should expand to

'(or (not a) b (not c) d (not e) f)

Once you expand, it is easy to count the number of positive literals in the conjunction and see if there is at most one positive literal.
After you conclude the case of one clause, then you expand your solution to include conjunction of clauses.

Good luck

Gugamilare has the right idea. Basically take your implication (==> a b) and turn it into (or (not a) b) form. Then simplify it as much as possible. If it simplifies to 1 positive literal and 1 or more negative literals, then it is a horn clause.

This might help you get started.

(defun simplify (statement) statement)

(defun hornp (statement)
  (destructuring-bind (==> a b) statement
    (declare (ignore ==>))
    (format t "~%Simplified to ~a" (simplify `(or (not ,a) ,b)))))

Use your knowledge of logic & Lisp to write a recursive simplification routine. Use logic rules like:

• --literal-- simplifies to --literal--
• (not (not --clause--)) simplifies too (simplify --clause--)