Tactical theorem provers or proof planners, such as Clam 4

provide proof tactics and/or proof methods to support abstract level proof construction and to improve the communication with the user. Tactics and methods typically abbreviate fre-quently recurring low level proof patterns. A system like mega 2 is capable of an explicit maintenance of abstract level proof objects and support a stepwise ex-pansion of them in pure calculus level proofs while in other systems, e.g. HOL, the application of a tactic immediately introduces a calculus level derivation. The common problem is to describe and operationalize the mapping of the abstract level inferences in terms of