This thesis is concerned with the logical foundations and computational modeling of constraint-based grammar formalisms. By computational modeling I understand the testing of the empirical predictions of a given grammar on a computer. This subsumes, e.g., the parsing problem: given a grammar and a string, does the grammar predict that the string is grammatical, or ungrammatical? The logic under consideration is a typed feature logic, that may be viewed as a basis for formalizing HPSG grammars. The thesis has a dual focus on theory and computation. I give algorithms for solving the prediction problem, and the algorithms are proven correct with respect to the underlying logic.