  We provide a semantic characterization of AGM belief contraction based on
frames consisting of a Kripke belief relation and a Stalnaker-Lewis selection
function. The central idea is as follows. Let K be the initial belief set and
K-A be the contraction of K by the formula A; then B belongs to the set K-A if
and only if, at the actual state, the agent believes B and believes that if
not-A is (were) the case then B is (would be) the case.
