Existing research has shown that theorem proving techniques of predicate calculus can be used as effective tools for query resolution in decision support systems. Implementation of these techniques however require searching large axiom sets leading to dead ends and backtracking. In this paper we use a mathematical programming approach to partition axiom sets into modules for efficient query resolution. The method is based on a two-stage analysis of the domain specific knowledge regarding queries types. The first stage analyzes the queries to determine the information requirement on the axiom set. The second stage determines the optimal modularization of the axiom set using this information. The advantage of our approach is that by selecting the appropriate modules for query resolution only a subset of axioms are considered in the resolution process. This approach works significantly better than the traditional methods when the axiom set can be partitioned into non-overlapping modules based on the commonality of a given query set. In the case of module overlap, the math program assigns the axioms to one of the overlapping modules maximizing overall query resolution efficiency of the system. An adaptive component performs dynamic reorganization of the modules when the query set is time variant. Real time issues of query resolution with modularized axiom set are briefly discussed. INFORMS Journal on Computing, ISSN 1091-9856, was published as ORSA Journal on Computing from 1989 to 1995 under ISSN 0899-1499.