Horn Clause

Jump to: navigation, search

A Horn Clause is a logic clause containing exactly one positive literal.




  • (Wikipedia, 2009) ⇒ http://en.wikipedia.org/wiki/Horn_clause
    • … A Horn clause with exactly one positive literal is a definite clause; a Horn clause with no positive literals is sometimes called a goal clause, especially in logic programming. A Horn formula is a conjunctive normal form formula whose clauses are all Horn; in other words, it is a conjunction of Horn clauses. A dual-Horn clause is a clause with at most one negative literal. Horn clauses play a basic role in logic programming and are important for constructive logic.
    • The following is an example of a (definite) Horn clause:
      • ¬p ∨ ¬q ∨ … ∨ ¬t ∨ u
    • Such a formula can also be written equivalently in the form of an implication:
      • (p ∧ q ∧ … ∧ t) → u
    • Horn clauses can be propositional or first order, depending on whether we consider propositional or first-order literals.