The application of deduction in various domains resulted in a variety of di
fferent techniques to guide the proof search. Many of these techniques inco
rporate additional knowledge to restrict or select possible proof steps. As
a consequence, usually the underlying calculus has to he modified to keep
track of this information during the proof search. In this paper we present
a general framework fur maintaining additional strategic knowledge within
a proof. We introduce a formal notion of annotations attached to the consti
tuents of formulas and illustrate how a generic method of inheriting these
annotations can br instantiated for various purposes.