Hornlog

Hornlog: A graph-based interpreter for general Horn clauses. In this very interesting paper a new method is presented for logic- programming interpreters based on graph rewriting and on a linear-time algorithm for showing the unsatisfiability of ground Horn clauses. The method (called Hornlog) applies to a class of logic programs that is a proper extension of the class that consists of what are normally called Horn clauses, but is still strictly included in the class of first-order formulas. In particular, negative Horn clauses can be used as assertions and also queries consisting of disjunctions of negations of Horn clauses are allowed. It is possible in this class to state some forms of negation without resort to negation-as-failure semantics. Moreover, it is possible to yield indefinite answers, i.e. disjunctions of substitutions. The method seems particularly useful for implementation in a parallel environment.