Transforming Horn Clauses for Forward Reasoning. - Knut Hinkelmann; Martin Harm; Thomas Labisch (PDK, 1991)