Possible events, actual events, and robots

Abstract

To plan means reasoning about possible actions, but a robot must also reason about actual events. This paper proposes a formal theory about actual and possible events. It presents a new modal logic as a notation for this theory and a technique for planning in the modal logic using a first‐order theorem prover augmented with simple modal reasoning. This avoids the need for a general modal‐logic theorem prover. Adding beliefs to this theory raises an interesting problem for which the paper offers a tentative solution.