FOL as Rule Language

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

  • Quantification most times omitted, free Variables are considered to be universally quantified
  • i.e. the Rule holds for all possible Assignments

Tags: logic, implication
Categories: Concept
Parent: Rule
Children: Variants of FOL Rules

Update entry (Admin) | See changes

Comment on This Data Unit