The aspect calculus for reasoning about states and actions has some advantages over existing situation calculus formalisms for theorem proving applications, and also provides an application domain and a source of problems for first-order theorem provers. The aspect calculus provides a representation for reasoning about states and actions that is suited to modular domains. An aspect names a portion of a state, that is, a substate, such as a room in a building or a city in a country. Aspects may have aspects of their own. A state is assumed to be either a {\em leaf state} that cannot be further decomposed, or to be composed of substates, and actions associated with one substate do not influence other, disjoint substates. This feature can reduce the number of frame axioms that are needed if the domain has a modular structure. It can also permit planning problems on independent substates to be solved independently to some degree. However, interactions between independent substates are also permitted.