• Horn Rules Semantics

Comments for this page

A function-free Horn rule is an implication from an antecedant (a set of atomic formulae) to a consequent (a single atomic formula). All the variables in the consequent must occur in at least one atom of the antecedant, and are all considered to be universally quantified. Thus a function-free Horn rule can be considered to be a formula of the following form:

• forall x₁ ... x_n c(y₁,...,y_m) <- p₁(y₁₁,...,y_1m1) ^... p_n(y_n1,...,y_nmn)
  where n,m,m₁,...,m_n>=0

  • and c,p₁,...,p_n are m,m₁,...,m_n-ary predicates
    and y₁,...,y_m,y₁₁,...,y_1m1,...,y_n1,y_nmn are either variables or constants

  with {v | v is a variable in {y₁₁,...,y_m1,...,y_n1,...,y_nmn} } = { x₁, ..., x_n }
  and {v | v is a variable in {y₁,...,y_m} } <= {v | v is a variable in {y₁₁,...,y_m1,...,y_n1,...,y_nmn} }

[[The variable notation above needs work]]

Note that one could consider the restriction where 1<=m,m₁,...,m_n<=2.

There are two basic semantics for sets of Horn rules, the FOL and the minimal model semantics. Both derive from the standard meaning of rules treated as first-order implications, where a rule is true if all possible instantiations of it are true, treating the instantiation as a material implication. The two semantics differ, however, in what interpretations they consider.

The FOL semantics considers all first-order intepretations, so that a function-free Horn rule is generally true in many interpretations. The minimal-model semantics only considers those interpretations that minimize the extension of predicates.

It turns out that for a given domain and mapping from constants into the domain there is exactly one such minimal model. These models all have the same set of consequences of the form p(a₁,...,a_m) where p is an m-ary predicate that occurs in the rule set and a₁,...,a_m are constants. Under these circumstances it suffices to consider the domain of interpretation to be the Herbrand universe over the syntactic elements of the rule set (adding an extra constant if the rules have no constants). As there are no functions in function-free Horn rules, this is then simply the set of constants in the rules (or a single constant, if needed, to make the domain non-empty). In fact, it is this Herbrand minimal model that is often considered to be the single model for a set of Horn rules. It is possible to go even further, and treat the implicit quantification in the rules as simply shorthand for conjunctions (here finite, but infinite if functions are allowed) of replacements of variables by elements of the Herbrand universe, i.e., constants (or ground terms, if functions are allowed).

So we then have four usual formal semantics for a set of function-free Horn rules:

1. all possible first-order interpretations,
2. all interpretations minimal in the extension of predicates,
3. the minimal model for the Herbrand universe, and
4. the minimal model for the Herbrand universe with quantification as replacement.

Note that there are other formal semantics for rules, that are generally used for non-Horn rules. These other semantics may have better characteristics when combined with RDF and OWL.

As stated above, it turns out that the second, third, and fourth semantics have the same consequences with respect to positive ground atoms, i.e., they provide the same entailments of the form

1. RS |= p(a₁,...,a_m)

Further, the first semantics also behaves the same with respect to these entailments.

Why, then, worry about the different semantics? Well, simply because differences start to show up when considering other sorts of entailments, i.e., generalizing either the left-hand or right-hand sides, or both, of entailment (A).

Comments

• 2005-12-20 MichaelSintek: According to the charter, we will use (unrestricted) Horn rules in phase 1, not just function-free Horn rules. Should we nevertheless define (syntactically and semantically) in phase 1 both function-free and unrestricted Horn rules?