In this paper we describe a logic-based AI architecture based on Brooks’ Subsumption Architecture. We axiomatize each of the layers of control in his system separately and use independent theorem provers to derive each layer’s outputs given its inputs. We implement the subsumption of lower layers by higher layers using circumscription to make assumptions in lower levels and nonmonotonically retract them when higher levels come up with some new conclusions. We give formal semantics to our approach. Finally, we describe an empirical experiment showing the feasibility of robot control using our architecture.