Non-Horn computing involves clauses of the form
A 1 ∨ A 2 ∨ ... ∨ A n < - B 1 ∧ B 2 ∧ ... ∧ B m,
where the A is and B js are atomic formulae and the B js may be negative. The query evaluation strategy described in this paper is an extension of the Alexander method developed for recursive query processing. The paper is clearly written and worth reading. My only criticism concerns the title. Computing with non-Horn clauses is notoriously inefficient, and it remains to be seen whether computing with such clauses can be practical. The use of the term “efficient” here should be understood relatively.
