I shall be demonstrating a system for describing programs operating by manipulations on sets of Horn clauses. This class of problem is interesting because it allows set-based notions of refinement to be used as a precursor to defining logic programs.