The control component of Open Mechanized Reasoning Systems (OMRS)
specifies the strategies according to which systems apply inference
rules in order to perform deductions. In this talk I present the
main ideas of a formalism for the control component of OMRS, and
show how it can be used to express the stategies of provers based
on resolution ("plain" resolution and its refinements such as lock
resolution).