Théorie Universelle de Horn

Une théorie du premier ordre axiomatisée par des phrases Horn universelles : des implications dont l'antécédent est une conjonction de formules atomiques (souvent des égalités) et dont le conséquent est une seule formule atomique ou la fausseté.