Deciding H1 by resolution

Nielson, Nielson and Seidl's class H1 is a decidable class of first-order Horn clause sets, describing strongly regular relations. We give another proof of decidability, and of the regularity of the defined languages, based on fairly standard automated deduction techniques.