A Horn clause in the language of a universal algebra is a disjunction of equations and of at most one inequality ("equation" and "inequality" are the terms used by A.Horn in his paper "On sencences which are true of direct unions of algebras", Journal of Symbolic Logic, 1951, 16(1), 14-21.). Quasi-identities and, in particular, identities are (equivalent to) Horn clauses, and the classes of algebras I know are axiomatized only by these.

Is there any research of interesting classes of algebras axiomatized by non-Horn clauses? I believe, the algebraic methods and structures used in such research, would be useful in algebraization of set theory. Currently, there is an "Algebraic set theory" (AST) in category theory presentation, according to which two operations are foundational for set theory. I am working on a presentation of set theory with one binary foundational operation playing the role of membership relationship as discussed in this question. I doubt, that AST can be presented with axioms only in Horn clause form, and I am quite sure some the axioms in my approach cannot be so presented.

For example, I seriously doubt that the axiom of "atomicity" in this question of mine, can be presented as a Horn clause.

concreteresults which would help figure out an approach to my "adjunction algebras". $\endgroup$ – Ioachim Drugus Aug 4 '14 at 23:361more comments