Decidability ofstit theory with a single agent andRefref Equivalence

The purpose of this paper is to prove the decidability ofstit theory (a logic of “seeing to it that”) with a single agent andRefref Equivalence. This result is obtained through an axiomatization of the theory and a proof that it has thefinite model property. A notion ofcompanions to stit formulas is introduced and extensively used in the proof.