Horn Clause Example: Graphs and Partial Orders

Classical algebraic structures such as groups and rings can be given entirely in terms of equations, so they don’t require the full expressiveness of Horn clauses.

Directed graphs (with at most one edge between nodes) can be represented by their adjacency relation: for two vertices x and y, the adjacency relation R(x,y) holds if there is an edge from x to y. Undirected graphs can be modeled by requiring that directed edges between two vertices go in both directions: R(x,y) implies R(y,x).

Partially-ordered sets can also be modeled in terms of Horn clauses. The three properties of a partial order are all Horn clauses:

  • reflexivity — x ≤ x
  • transitivity — x ≤ y and y ≤ z implies x ≤ z.
  • asymmetry — x ≤ y and y ≤ x implies x = y.

(Thus preorders, which drop the asymmetry axiom, are also given by Horn clauses.)

Total orders, which impose the requirement x ≤ y or y ≤ x, cannot be given by Horn clauses.

Previous post here. Next post here.