Using theorem proving to verify properties of agent programs We present a sound and complete logic for automatic verification of simpleAPL programs. simpleAPL is a simplified version of agent programming languages such as 3APL and 2APL designed for the implementation of cognitive agents with beliefs, goals and plans. Our logic is a variant of PDL, and allows the specification of safety and liveness properties of agent programs. We prove a correspondence between the operational semantics of simpleAPL and the models of the logic for two example program execution strategies. We show how to translate agent programs written in simpleAPL into expressions of the logic, and give an example in which we show how to verify correctness properties for a simple agent program using theorem-proving.