A formal treatment of typed feature structures (TFSs) is developed to augment TFSs, so that negative descriptions of them can be treated. Negative descriptions of TFSs can make linguistic descriptions compact and thus easy to understand. Negative descriptions can be classified into three primitive negative descriptions: (1) negations of type symbols, (2) negations of feature existences, and (3) negations of feature-address value agreements. The formalization proposed in this paper is based on A'it-Kaci's complex terms. The first description is treated by extending type symbol lattices to include complement type symbols. The second and third are treated by augmeriting term structures with structures representing these negations. Algorithrrts for augmented-TFS unification have been developed using graph unification, and programs using these algorithms have been written in Conmaon Lisp.