Decidability of stit theory with a single agent and Refref equivalence (Q1327485)

The paper provides an axiomatisation for the stit theory of \textit{N. Belnap} and \textit{M. Perloff} [``Seeing to it that: a canonical form for agentives'', in: H. E. Kyburg jun., R. P. Loui and G. N. Carlson (eds.), Knowledge representation and defeasible reasoning (1990; Zbl 0743.68024)]. The axiomatisation includes the Refref principle (refraining from refraining is the same as doing). The theory is shown to have the finite model property with respect to the class of models in which there are no busy choice sequences (infinitely many non-vacuous choices in a finite time). The completeness of the axiomatisation with respect to this class of models, and the decidability of the theory, follow in the usual way.