Program tactics and logic tactics

In the past, tactics have been mostly implemented as programs written in some programming language, e.g. ML. We call the tactics of this kind, Program Tactics. In this paper we present a first order classical metatheory, called MT, with the following properties: (1) tactics are terms of the language of MT. We call these tactics, Logic Tactics; (2) there exists a mapping between Logic Tactics and the Program Tactics implemented within the GETFOL theorem prover. Property (1) allows us to use GETFOL to prove properties of and to build new Logic Tactics. Property (2) can be exploited to perform a bidirectional translation between Logic Tactics and Program Tactics.