  This theorem is a generalisation, due to Mal’tsev, of a group-theoretic construction called construction by generators and relations. It is the main idea behind algebraic specification, which is one approach to the specification of systems in computer science. The required behaviour of the system is written down as a set of strict universal Horn sentences, and then the initial model of these sentences is an abstract version of the required system. 