Horn Clause

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

• Context:
  • It can be used to represent:
    • a Logic Fact if no Negative Literals.
    • a Definite Clause (or Production Rule) if exactly one Positive Literal.
    • a Goal Clause if no Positive Literals.
  • It can be a part of:
    • a Horn Formula (a Conjunction of Horn Clauses).
  • Resolution of two Horn Clause always results in a Horn Clause.
  • Resolution of a Goal Clause and a Definite Clause is always a Goal Clause.
  • Prolog is based on computing with Horn Clauses.
  • It can be written in the form of a Logical Implication Relation.
• Example(s):
  • (Parent(x,y) ∧ Parent(y,z) ∧ person(x) ∧ person(y) ∧ person(z)) → Grandparent(x,y).
  • a Dual-Horn Clause.
  • a Definite Clause.
• See: Definite Clause, Ground Fact, Forward Chaining Algorithm, Backward Chaining Algorithm, SLD-Resolution, Conjunctive Normal Form, Kowalski Normal Form, Horn Clause Satisfiability Task, Programming Conditional Statement.

---

---

References

2015

• (Wikipedia, 2015) ⇒ http://en.wikipedia.org/wiki/horn_clause Retrieved:2015-5-23.
  • In mathematical logic and logic programming, a Horn clause is a logical formula of a particular rule-like form which gives it useful properties for use in logic programming, formal specification, and model theory. Horn clauses are named for the logician Alfred Horn, who first pointed out their significance in 1951, in the article "On sentences which are true of direct unions of algebras", Journal of Symbolic Logic, 16, 14–21.

2009

• (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.

---