We present a logic for reasoning about properties of agent programs under different agent execution strategies. Using the agent programming language SimpleAPL as an example, we show how safety and liveness properties can be expressed by translating agent programs into expressions of the logic. We give sound and complete axiomatizations of two different program execution strategies for SimpleAPL programs, and, for each of those strategies, prove a correspondence between the operational semantics of SimpleAPL and the models of the corresponding logic. Categories and Subject Descriptors I.2 [Artificial Intelligence]; F.3 [Logics and Meanings of Programs] Keywords Formalisms and logics