Logical Features of Horn Clauses
Wilfrid Hodges · 1993
Abstract Horn clause logic is a part of first-order logic. It was first isolated by J. C. C. McKinsey (1943), who was working on decision problems. Between 1956 and 1970, Anatoliī Mal’tsev published a series of papers in which he showed that Horn clauses form the right setting for a large part of universal algebra—including the theory of presentations and initial models. Algebraic specification lies within this part of universal algebra.