Applications of the situation calculus to formalizing control and strategic information: The Prolog cut operator

We argue that the situation calculus is a natural formalism for representing and reasoning about control and strategic information. As a case study, in this paper we provide a situation calculus semantics for the Prolog cut operator, the central search control operator in Prolog. We show that our semantics is well-behaved when the programs are properly stratified, and that according to this semantics, the conventional implementation of the negation-as-failure operator using cut is provably correct with respect to the stable model semantics.