Tactic
A term derived from Coq's usage of it meaning a program which operates on a declarative system in a procedural manner. That is, it operates on the declarative system in the mode of directing the proof of it, possibly re-using existing proof procedures or overriding default ones.This can be compared and contrasted with Maude's rewrite logic strategies.