Created on March 12, 2013, 2:02 a.m. by Hevok & updated by Hevok on May 2, 2013, 5:35 p.m.
Logical Rules always comply to a specific Schema. Usually one has a body which is the first part of the Implication and one has the head or header which is the second part of the Implication.
These kind of Implication where one has one simple Atomic Fact as the second part, the head of the Implications, it can be written as a Horn Clause.
These Implication can be transformed into a Disjunction in which all Atoms in the body will be negated and connected via Disjunction and the header/head is not negated.
In a Horn Clause all of its constituents are negated besides at most one not negated Atom.
Most times the Quantification of this Rules are omitted because free Variables are considered to be universal quantified. This means that the Rule that is stated holds for all possible Assignments.
Sometimes these Rules are written the other way around with first the head, then the Implication arrow, but its pointing in the reverse direction and then there is the body. This stems from Logical Programming where one writes Rules in this way, but they are equivalent with each other.
Rules as FOL Implications (Horn Clause)
A1 ∧ A2 ∧ ... ∧ An → H Body → Head
often written from right to left ( ← or :- )
H ← A1 ∧ A2 ∧ ... ∧ An
Head ← Body
semantically equivalent with
¬A1 ∨ ¬A2 ∨ ... ∨ ¬An ∨ H
where Ai, H are atomic Formulas
Comment on This Data Unit