We introduce a typed feature logic system providing both universal implicational principles as well as definite clauses over feature terms. We show that such an architecture supports a modular encoding of linguistic theories and allows for a compact representation using underspecification. The system is fully implemented and has been used as a workbench to develop and test large HPSG grammars. The techniques described in this paper are not restricted to a specific implementation, but could be added to many current feature-based grammar development systems. Introduction A significant part of the development of formalisms for computational linguistics has been concerned.