Negation Normal Form An ALC formula where only concept names are negated. Works by pulling in the negations using the ALC identities in linear time.