Deciding H1 by resolution
Goubault-LarrecqJean · Information Processing Letters · 2005
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 th...