Abstract
In a seminal paper, Lin and Reiter introduced the notion of progression for basic action theories in the situation calculus. Earlier works by Moore, Scherl and Levesque extended the situation calculus to account for knowledge. In this paper, we study progression of knowledge in the situation calculus. We ?rst adapt the concept of bisimulation from modal logic and extend Lin and Reiter’s notion of progression to accommodate knowledge. We show that for physical actions, progression of knowledge reduces to forgetting predicates in ?rstorder modal logic. We identify a class of ?rst-order modal formulas for which forgetting an atom is de?nable in ?rst-order modal logic. This class of formulas goes beyond formulas without quantifyingin. We also identify a simple case where forgetting a predicate reduces to forgetting a ?nite number of atoms. Thus we are able to show that for local-effect physical actions, when the initial KB is a formula in this class, progression of knowledge is de?nable in ?rst-order modal logic. Finally, we extend our results to the multi-agent case.