Tactics are encoded as verifiable meta-functions in a powerful programming logic with reflective capabilities. These formalized tactics are applied to specific problems by means of deductive reflection rules. The main advantage of this approach lies in the fact that meta-theoretic results, once proven, are used without further justification to construct proofs of object-level problems. As another consequence, new theorem-proving capabilities like decision procedures are added and tightly integrated with the basic formal tactics mechanism in a sound way.
展开▼
